Mathlib Changelog
v4
Changelog
About
Github
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