Commit 2026-03-24 21:53 aef0fa08

View on Github →

chore(Topology/Subpath): deprecate Path.subpathAux in favor of Set.Icc.convexCombo (#36921) The declaration Path.subpathAux is just a special case of Set.Icc.convexCombo, so this PR deprecates Path.subpathAux in favor of Set.Icc.convexCombo.

Estimated changes

Modified Mathlib/Topology/Subpath.lean

modified theorem Path.range_subpathAux

deleted def Path.subpathAux

deleted theorem Path.subpathAux_continuous

deleted theorem Path.subpathAux_one

deleted theorem Path.subpathAux_zero

Modified Mathlib/Topology/UnitInterval.lean

added theorem Set.Icc.continuous_convexCombo

added theorem Set.Icc.continuous_convexCombo_prod

added theorem Set.Icc.convexCombo_eq

added theorem Set.Icc.convexCombo_zero_one