Commit 2026-11-10 14:10 0114c591

View on Github →

feat(Geometry/Convex): segments in convex space (#44799) Adds segments and open segments for convex spaces, and provides some basic API. Follows Mathlib.Analysis.Convex.Segment.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Convex/Segment.lean

added def Convexity.Icc

added theorem Convexity.Icc_self

added theorem Convexity.Icc_subset_iff

added theorem Convexity.Icc_subset_iff_mem_of_isConvexSet

added theorem Convexity.Icc_symm

added def Convexity.Ico

added theorem Convexity.Ico_insert

added theorem Convexity.Ico_self

added theorem Convexity.Ico_subset_Icc

added theorem Convexity.Ico_subset_iff

added def Convexity.Ioo

added theorem Convexity.Ioo_insert_left

added theorem Convexity.Ioo_insert_right

added theorem Convexity.Ioo_self

added theorem Convexity.Ioo_subset_Icc

added theorem Convexity.Ioo_subset_Ico

added theorem Convexity.Ioo_subset_iff

added theorem Convexity.Ioo_subset_singleton

added theorem Convexity.Ioo_symm

added theorem Convexity.IsAffineMap.image_Icc

added theorem Convexity.IsAffineMap.image_Ico

added theorem Convexity.IsAffineMap.image_Ioo

added theorem Convexity.IsAffineMap.mem_Icc_image

added theorem Convexity.IsAffineMap.mem_Ico_image

added theorem Convexity.IsAffineMap.mem_Ioo_image

added theorem Convexity.Prod.Icc_subset

added theorem Convexity.Prod.Ico_subset

added theorem Convexity.Prod.Ioo_subset

added theorem Convexity.convexCombPair_mem_Icc

added theorem Convexity.convexCombPair_mem_Ico

added theorem Convexity.convexCombPair_mem_Ioo

added theorem Convexity.forall_mem_Icc_iff

added theorem Convexity.forall_mem_Ico_iff

added theorem Convexity.forall_mem_Ioo_iff

added theorem Convexity.isConvexSet_iff_Icc_subset_of_mem

added theorem Convexity.left_mem_Icc

added theorem Convexity.left_mem_Ico

added theorem Convexity.right_mem_Icc