Commit 2024-01-16 16:52 df0c38b7

View on Github →

feat: Intersection of convex hulls is convex hull of intersection (#9203) when everything is affine independent. Also a related affine span lemma. From LeanCamCombi

Estimated changes

Modified Mathlib/Analysis/Convex/Combination.lean

added theorem AffineIndependent.convexHull_inter'

added theorem AffineIndependent.convexHull_inter

added theorem Finset.mem_convexHull'

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

added theorem AffineIndependent.card_le_card_of_subset_affineSpan

added theorem AffineIndependent.card_lt_card_of_affineSpan_lt_affineSpan

added theorem AffineIndependent.finrank_vectorSpan_add_one

added theorem finrank_vectorSpan_range_add_one_le