Commit 2026-08-31 07:29 9b68e6ac

View on Github →

feat(Geometry): the standard simplex is compact (#43202) This PR expands the API for StdSimplex. It is shown that the 1-dimensional standard simplex identifies to an interval, and under suitable assumptions on R, StdSimplex R M is compact when M is finite. (This was obviously known for stdSimplex which will be deprecated in #42181.)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Convex/ConvexSpace/CompactSpaceStdSimplex.lean

added theorem Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall

added theorem Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_one

added theorem Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_zero

added theorem Convexity.StdSimplex.isBounded_range_toFun_comp_weights

added theorem Convexity.StdSimplex.range_toFun_comp_weights_subset_closedBall

Modified Mathlib/Geometry/Convex/ConvexSpace/Defs.lean

added def Convexity.StdSimplex.equivIcc

added theorem Convexity.StdSimplex.equivIcc_single_one

added theorem Convexity.StdSimplex.equivIcc_single_zero

added theorem Convexity.StdSimplex.equivIcc_symm_one

added theorem Convexity.StdSimplex.equivIcc_symm_zero

added theorem Convexity.StdSimplex.iConvexComb_single

added theorem Convexity.StdSimplex.single_injective

added theorem Convexity.StdSimplex.total_fin_two

added theorem Convexity.StdSimplex.weights_apply_eq_one

added theorem Convexity.StdSimplex.weights_apply_le_one

added theorem Convexity.sConvexComb_map_iConvexComb