mathlib

136d0ce9 - feat(topology/homotopy/path): Add homotopy between paths (#9141)

feat(topology/homotopy/path): Add homotopy between paths (#9141) There is also a lemma about `path.to_continuous_map` which I needed in a prior iteration of this PR that I missed in #9133