Theorem Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_one

Modification history

2026-08-31 07:29
Mathlib/Geometry/Convex/ConvexSpace/CompactSpaceStdSimplex.lean
feat(Geometry): the standard simplex is compact (#43202) …
Added Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_oneView on Github →