Commit 2021-10-11 21:39 df132fe6

View on Github →

feat(topology/path_connected): add path.reparam for reparametrising a path. (#9643) I've also added simps to some of the definitions in this file.

Estimated changes

Modified src/topology/path_connected.lean

added theorem path.coe_to_fun

added theorem path.range_reparam

modified def path.refl

added theorem path.refl_reparam

added def path.reparam

added theorem path.reparam_id

added def path.simps.apply

modified def path.symm