Commit 2026-06-04 18:23 5ea21144

View on Github →

feat(Geometry/Convex): star-convex sets in a convex space (#40230) Define IsStarConvexSet,a predicate for a set in a ConvexSpace to be star-convex at a point. Add a few lemmas about IsAffineMap as preliminaries to lemmas about star-convex sets in a module. The existing Module-specific StarConvex predicate will be deprecated in a future PR.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Star.lean

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

added theorem Convexity.IsAffineMap.add

added theorem Convexity.IsAffineMap.map_smul_add_smul

added theorem Convexity.IsAffineMap.map_sum_weights

added theorem Convexity.IsAffineMap.neg

added theorem Convexity.IsAffineMap.sub

added theorem Convexity.IsStarConvexSet.add

added theorem Convexity.IsStarConvexSet.neg

added theorem Convexity.IsStarConvexSet.sub

Created Mathlib/Geometry/Convex/Star.lean

added theorem Convexity.IsConvexSet.isStarConvexSet

added theorem Convexity.IsStarConvexSet.iInter₂

added theorem Convexity.IsStarConvexSet.mem

added def Convexity.IsStarConvexSet