Theorem Path.range_subpathAux

Modification history

2026-05-15 08:37
Mathlib/Topology/Subpath.lean
feat(Geometry/Convex): indexed convex combinations (#37592) …
Modified Path.range_subpathAuxView on Github →
2026-03-24 21:53
Mathlib/Topology/Subpath.lean
chore(Topology/Subpath): deprecate `Path.subpathAux` in favor of `Set.Icc.convexCombo` (#36921) …
Modified Path.range_subpathAuxView on Github →
2026-01-08 11:26
Mathlib/Topology/Subpath.lean
feat(Topology): add definition for subpaths (#27261) …
Added Path.range_subpathAuxView on Github →