Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-31 12:11 a8ba81b3

View on Github →

feat(analysis/convex): define convex hull (#1915)

  • feat(analysis/convex): define convex hull fixes #1851
  • Fix compile
  • Drop an unused argument
  • Split line
  • Rename some _iffs, drop others
  • Mention std_simplex in the docs
  • More docs
  • Rename α to ι, other small fixes
  • Use range instead of f '' univ
  • More docs

Estimated changes

added theorem finset.prod_sum_elim
modified theorem convex.add
modified theorem convex.affinity
modified theorem convex.center_mass_mem
deleted theorem convex.closure
added theorem convex.convex_hull_eq
modified theorem convex.inter
deleted theorem convex.interior
modified theorem convex.is_linear_image
modified theorem convex.is_linear_preimage
modified theorem convex.linear_image
modified theorem convex.linear_preimage
modified theorem convex.neg
modified theorem convex.neg_preimage
modified theorem convex.prod
added theorem convex.segment_subset
modified theorem convex.smul
modified theorem convex.smul_preimage
modified theorem convex.sub
modified theorem convex.sum_mem
modified theorem convex.translate
modified def convex
modified theorem convex_Inter
deleted theorem convex_ball
deleted theorem convex_closed_ball
added theorem convex_convex_hull
modified theorem convex_empty
modified theorem convex_halfspace_ge
modified theorem convex_halfspace_gt
modified theorem convex_halfspace_le
modified theorem convex_halfspace_lt
added def convex_hull
added theorem convex_hull_eq
added theorem convex_hull_min
added theorem convex_hull_mono
modified theorem convex_hyperplane
deleted theorem convex_iff:
deleted theorem convex_iff₂:
deleted theorem convex_iff₃:
modified theorem convex_on.add
modified theorem convex_on.convex_epigraph
modified theorem convex_on.convex_le
modified theorem convex_on.convex_lt
deleted theorem convex_on.le_on_interval
modified theorem convex_on.map_sum_le
modified theorem convex_on.smul
modified theorem convex_on.subset
modified def convex_on
deleted theorem convex_on_dist
deleted theorem convex_on_iff
modified theorem convex_real_iff
modified theorem convex_sInter
modified theorem convex_segment
deleted theorem convex_segment_iff
modified theorem convex_singleton
added theorem convex_std_simplex
modified theorem convex_univ
modified theorem finset.center_mass_empty
modified theorem finset.center_mass_insert
modified theorem finset.center_mass_pair
added theorem ite_eq_mem_std_simplex
modified theorem left_mem_segment
deleted theorem mem_segment_iff'
deleted theorem mem_segment_iff
added theorem mem_segment_translate
modified theorem right_mem_segment
modified def segment
modified theorem segment_eq_Icc'
added theorem segment_eq_image'
added theorem segment_eq_image
added theorem segment_eq_image₂
added theorem segment_same
modified theorem segment_symm
deleted theorem segment_translate
modified theorem segment_translate_image
modified theorem segment_translate_preimage
added def std_simplex
added theorem std_simplex_eq_inter
modified theorem submodule.convex
added theorem subset_convex_hull
modified theorem subspace.convex
added theorem bounded_convex_hull
added theorem bounded_std_simplex
added theorem compact_std_simplex
added theorem convex.closure
added theorem convex.interior
added theorem convex_ball
added theorem convex_closed_ball
added theorem convex_hull_diam
added theorem convex_hull_ediam
added theorem convex_on_dist
added theorem is_closed_std_simplex
added theorem nnreal.div_one
added theorem nnreal.div_self
added theorem ite_smul
added theorem smul_ite