Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-12 15:28 92bd7b1f

View on Github →

feat(analysis/convex): convexity of n-ary sums (#18943)

Estimated changes

Modified src/analysis/convex/basic.lean

added theorem coe_convex_add_submonoid

added def convex_add_submonoid

added theorem convex_list_sum

added theorem convex_multiset_sum

added theorem convex_sum

added theorem convex_zero

added theorem mem_convex_add_submonoid

Modified src/analysis/convex/combination.lean

added def convex_hull_add_monoid_hom

added theorem convex_hull_list_sum

added theorem convex_hull_multiset_sum

added theorem convex_hull_sum

Modified src/analysis/convex/hull.lean

added theorem convex_hull_zero

Modified src/measure_theory/measure/haar/of_basis.lean