Theorem Convexity.StdSimplex.convexCombPair_restrict_restrict_compl

Modification history

2026-05-21 09:56
Mathlib/Geometry/Convex/ConvexSpace/Defs.lean
feat(Geometry/Convex): convex sets in a `ConvexSpace` (#38905) …
Added Convexity.StdSimplex.convexCombPair_restrict_restrict_complView on Github →