Commit 2025-04-13 22:36 2ccecc0e

View on Github →

feat(Topology/Path): prove Path.extend_symm (#23980)

Estimated changes

Modified Mathlib/Order/Interval/Set/ProjIcc.lean

Modified Mathlib/Topology/Path.lean

added theorem Path.extend_symm

added theorem Path.extend_symm_apply

added theorem Path.ofLine_extend

modified theorem Path.symm_range

Modified Mathlib/Topology/UnitInterval.lean

added theorem unitInterval.symm_projIcc