Commit 2026-09-01 17:26 8d48831c

View on Github →

feat(Geometry): affine maps from the standard simplex (#43260) We introduce a constructor for affine maps from a standard simplex to a convex space, and we show that affine maps from the standard simplex to modules are continuous.

Estimated changes

Modified Mathlib.lean

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

added theorem Convexity.ConvexSpace.AffineMap.StdSimplex.affineMapMk_apply

added theorem Convexity.ConvexSpace.AffineMap.StdSimplex.affineMapMk_single

added theorem Convexity.ConvexSpace.AffineMap.StdSimplex.affineMapMk_surjective

added theorem Convexity.ConvexSpace.AffineMap.StdSimplex.affineMap_ext

added theorem Convexity.ConvexSpace.AffineMap.StdSimplex.affineMap_id

added theorem Convexity.ConvexSpace.AffineMap.StdSimplex.coe_affineMap

added theorem Convexity.ConvexSpace.AffineMap.StdSimplex.comp_affineMapMk

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

added theorem Convexity.StdSimplex.affineMapMk_apply_eq_sum_of_fintype

added theorem Convexity.StdSimplex.coe_affineMapMk_of_fintype

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