mathlib3
df132fe6 - feat(topology/path_connected): add `path.reparam` for reparametrising a path. (#9643)

Commit

4 years ago

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.

Author

shingtaklam1324

Parents

136d0ce9

mathlib3 df132fe6 - feat(topology/path_connected): add `path.reparam` for reparametrising a path. (#9643)

mathlib3
df132fe6 - feat(topology/path_connected): add `path.reparam` for reparametrising a path. (#9643)