Theorem Affine.Simplex.dist_lt_of_mem_closedInterior_of_strictConvexSpace

Modification history

2025-12-06 00:03
Mathlib/Analysis/Convex/StrictCombination.lean
feat(Analysis/Convex/StrictCombination): convex combinations in strictly convex sets and spaces (#31452) …
Added Affine.Simplex.dist_lt_of_mem_closedInterior_of_strictConvexSpaceView on Github →