Commit 2025-05-06 13:07 499fdf7b

View on Github →

refactor(Path): turn Path.extend into a ContinuousMap (#24066) This way we can, e.g., extend a homotopy between paths to a homotopy between their extensions.

Estimated changes

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

Modified Mathlib/Topology/Path.lean

added theorem Continuous.pathExtend

deleted theorem Continuous.path_extend

added theorem ContinuousAt.pathExtend

deleted theorem ContinuousAt.path_extend

added theorem Filter.Tendsto.pathExtend

deleted theorem Filter.Tendsto.path_extend

added theorem Path.coe_mk'

modified def Path.extend

modified theorem Path.refl_extend

modified theorem Path.refl_range

modified theorem Path.refl_symm