Theorem Set.Icc.continuous_convexCombo_prod

Modification history

2026-05-15 08:37
Mathlib/Topology/UnitInterval.lean
feat(Geometry/Convex): indexed convex combinations (#37592) …
Deleted Set.Icc.continuous_convexCombo_prodView on Github →
2026-03-24 21:53
Mathlib/Topology/UnitInterval.lean
chore(Topology/Subpath): deprecate `Path.subpathAux` in favor of `Set.Icc.convexCombo` (#36921) …
Added Set.Icc.continuous_convexCombo_prodView on Github →