Theorem Path.subpathAux_one

Modification history

2026-03-24 21:53
Mathlib/Topology/Subpath.lean
chore(Topology/Subpath): deprecate `Path.subpathAux` in favor of `Set.Icc.convexCombo` (#36921) …
Deleted Path.subpathAux_oneView on Github →
2026-01-08 11:26
Mathlib/Topology/Subpath.lean
feat(Topology): add definition for subpaths (#27261) …
Added Path.subpathAux_oneView on Github →