Commit 2026-09-03 08:22 1ad2ea68

View on Github →

doc(Geometry/Convex): better explain StdSimplex R M and ConvexSpace R R (#43340) Also rename M, N, P to X, Y, Z in ConvexSpace.Defs to help clear the misunderstanding about the role of StdSimplex These doc improvements stemmed from discussions at the Polyhedra in Berlin workshop.

Estimated changes

Modified Mathlib/Analysis/Convex/MetricSpace.lean

Modified Mathlib/Analysis/Convex/Topology.lean

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

modified theorem Convexity.IsAffineMap.comp

modified theorem Convexity.IsAffineMap.const

modified theorem Convexity.IsAffineMap.map_convexCombPair

modified theorem Convexity.IsAffineMap.map_iConvexComb

modified structure Convexity.IsAffineMap

modified def Convexity.StdSimplex.duple

modified def Convexity.StdSimplex.join

modified def Convexity.StdSimplex.map

modified theorem Convexity.StdSimplex.map_comp'

modified theorem Convexity.StdSimplex.map_comp

modified theorem Convexity.StdSimplex.map_const

modified theorem Convexity.StdSimplex.map_duple

modified theorem Convexity.StdSimplex.map_id'

modified theorem Convexity.StdSimplex.map_id

modified theorem Convexity.StdSimplex.map_map

modified theorem Convexity.StdSimplex.map_single

modified theorem Convexity.StdSimplex.mk_single

modified theorem Convexity.StdSimplex.nonempty

modified theorem Convexity.StdSimplex.range_toFun_comp_weights

modified def Convexity.StdSimplex.single

modified theorem Convexity.StdSimplex.single_injective

modified theorem Convexity.StdSimplex.support_weights_nonempty

modified theorem Convexity.StdSimplex.total_of_fintype

modified theorem Convexity.StdSimplex.weights_apply_eq_one

modified theorem Convexity.StdSimplex.weights_inj

modified theorem Convexity.StdSimplex.weights_ne_zero

modified theorem Convexity.StdSimplex.weights_nonneg

modified structure Convexity.StdSimplex

modified def Convexity.convexCombPair

modified theorem Convexity.convexCombPair_convexCombPair_assoc_left

modified theorem Convexity.convexCombPair_convexCombPair_assoc_right

modified theorem Convexity.convexCombPair_convexCombPair_left_eq_sConvexComb

modified theorem Convexity.convexCombPair_convexCombPair_right_eq_sConvexComb

modified theorem Convexity.convexCombPair_def

modified theorem Convexity.convexCombPair_iConvexComb_left

modified theorem Convexity.convexCombPair_iConvexComb_right

modified theorem Convexity.convexCombPair_one

modified theorem Convexity.convexCombPair_same

modified theorem Convexity.convexCombPair_symm

modified theorem Convexity.convexCombPair_zero

modified def Convexity.iConvexComb

modified theorem Convexity.iConvexComb_congr

modified theorem Convexity.iConvexComb_const

modified theorem Convexity.iConvexComb_convexCombPair_comm

modified theorem Convexity.iConvexComb_convexCombPair_comm_left

modified theorem Convexity.iConvexComb_convexCombPair_comm_right

modified theorem Convexity.iConvexComb_id'

modified theorem Convexity.iConvexComb_id

modified theorem Convexity.iConvexComb_map

modified theorem Convexity.iConvexComb_reindex

modified theorem Convexity.iConvexComb_single

modified theorem Convexity.isAffineMap_convexCombPair

modified theorem Convexity.sConvexComb_convexCombPair

modified theorem Convexity.sConvexComb_map

modified theorem Convexity.sConvexComb_map_iConvexComb

modified theorem Convexity.sConvexComb_sConvexComb

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

modified theorem Convexity.StdSimplex.isAffineMap_weights