Commit 2023-09-14 21:19 50988b8b

View on Github →

feat(Analysis/Convex): Radon's convexity theorem (#6598) Add Radon's theorem on convex sets

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Combination.lean

added theorem Finset.centerMass_id_mem_convexHull_of_nonpos

added theorem Finset.centerMass_mem_convexHull_of_nonpos

added theorem Finset.centerMass_neg_left

added theorem Finset.centerMass_of_sum_add_sum_eq_zero

added theorem Finset.centerMass_smul_left

Created Mathlib/Analysis/Convex/Radon.lean

added theorem radon_partition