Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-11 17:31 b9ad7333

View on Github →

split(analysis/convex/combination): split off analysis.convex.basic (#9115) This moves finset.center_mass into its own new file. About the copyright header, finset.center_mass comes from #1804, which was written by Yury in December 2019.

Estimated changes

deleted theorem convex.center_mass_mem
deleted theorem convex.sum_mem
deleted theorem convex_hull_eq
deleted theorem convex_iff_sum_mem
deleted theorem convex_on.map_sum_le
deleted theorem finset.center_mass_empty
deleted theorem finset.center_mass_insert
deleted theorem finset.center_mass_ite_eq
deleted theorem finset.center_mass_pair
deleted theorem finset.center_mass_smul
deleted theorem finset.center_mass_subset
deleted theorem finset.convex_hull_eq
deleted theorem set.finite.convex_hull_eq
added theorem convex.center_mass_mem
added theorem convex.sum_mem
added theorem convex_hull_eq
added theorem convex_iff_sum_mem
added theorem convex_on.map_sum_le
added theorem finset.convex_hull_eq