Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-22 12:11 15730e8d

View on Github →

chore(analysis/convex): trivial generalizations of ℝ (#9298)

Estimated changes

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/calculus/local_extr.lean

Modified src/analysis/convex/basic.lean

deleted theorem convex_halfspace_im_ge

deleted theorem convex_halfspace_im_gt

deleted theorem convex_halfspace_im_le

deleted theorem convex_halfspace_im_lt

deleted theorem convex_halfspace_re_ge

deleted theorem convex_halfspace_re_gt

deleted theorem convex_halfspace_re_le

deleted theorem convex_halfspace_re_lt

modified theorem convex_std_simplex

modified theorem ite_eq_mem_std_simplex

modified def std_simplex

Modified src/analysis/convex/caratheodory.lean

Modified src/analysis/convex/combination.lean

modified theorem convex.center_mass_mem

modified theorem convex.sum_mem

added def finset.center_mass

modified theorem finset.center_mass_mem_convex_hull

modified theorem mem_Icc_of_mem_std_simplex

Created src/analysis/convex/complex.lean

added theorem convex_halfspace_im_ge

added theorem convex_halfspace_im_gt

added theorem convex_halfspace_im_le

added theorem convex_halfspace_im_lt

added theorem convex_halfspace_re_ge

added theorem convex_halfspace_re_gt

added theorem convex_halfspace_re_le

added theorem convex_halfspace_re_lt

Modified src/analysis/convex/extrema.lean

Modified src/analysis/convex/extreme.lean

Modified src/analysis/convex/function.lean

Modified src/analysis/convex/topology.lean

modified theorem bounded_std_simplex

modified theorem compact_std_simplex

modified theorem is_closed_std_simplex