Commit 2025-08-29 09:05 d1b44961

View on Github →

chore(Analysis/Convex): move to new file StdSimplex (#29097) Definitions relative to the standard simplex are moved to a new file Analysis.Convex.StdSimplex.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Basic.lean

deleted theorem convex_stdSimplex

deleted theorem ite_eq_mem_stdSimplex

deleted theorem segment_single_subset_stdSimplex

deleted theorem single_mem_stdSimplex

deleted def stdSimplex

deleted def stdSimplexEquivIcc

deleted theorem stdSimplex_eq_inter

deleted theorem stdSimplex_fin_two

deleted theorem stdSimplex_of_isEmpty_index

deleted theorem stdSimplex_of_subsingleton

deleted theorem stdSimplex_unique

Modified Mathlib/Analysis/Convex/Combination.lean

deleted theorem Set.Finite.convexHull_eq_image

deleted theorem convexHull_basis_eq_stdSimplex

deleted theorem mem_Icc_of_mem_stdSimplex

Created Mathlib/Analysis/Convex/StdSimplex.lean

added theorem Set.Finite.convexHull_eq_image

added theorem bounded_stdSimplex

added theorem convexHull_basis_eq_stdSimplex

added theorem convex_stdSimplex

added theorem isClosed_stdSimplex

added theorem isCompact_stdSimplex

added theorem ite_eq_mem_stdSimplex

added theorem mem_Icc_of_mem_stdSimplex

added theorem segment_single_subset_stdSimplex

added theorem single_mem_stdSimplex

added def stdSimplex

added def stdSimplexEquivIcc

added def stdSimplexHomeomorphUnitInterval

added theorem stdSimplex_eq_inter

added theorem stdSimplex_fin_two

added theorem stdSimplex_of_isEmpty_index

added theorem stdSimplex_of_subsingleton

added theorem stdSimplex_subset_closedBall

added theorem stdSimplex_unique

Modified Mathlib/Analysis/Convex/Topology.lean

deleted theorem bounded_stdSimplex

deleted theorem isClosed_stdSimplex

deleted theorem isCompact_stdSimplex

deleted def stdSimplexHomeomorphUnitInterval

deleted theorem stdSimplex_subset_closedBall