Commit 2026-02-25 22:02 6672fdb5

View on Github →

feat(Geometry/Euclidean): Simplex.closedInterior is closed (#35358) Intermediate lemma towards #34826. The immediate follow up is that the closed interior is measurable, but I'll leave it till the Measure folder appears under Geometry/Euclidean.

Estimated changes

Modified Mathlib/Analysis/Convex/Combination.lean

added theorem Affine.Simplex.convexHull_eq_closedInterior

Modified Mathlib/Analysis/Convex/StdSimplex.lean

modified theorem isClosed_stdSimplex

modified theorem isCompact_stdSimplex

added theorem stdSimplex_subset_Icc

Modified Mathlib/Analysis/Convex/Topology.lean

added theorem Affine.Simplex.isClosed_closedInterior

added theorem Affine.Simplex.isCompact_closedInterior

Modified Mathlib/Analysis/Convex/TotallyBounded.lean