Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-05 13:56 78e36a71

View on Github →

feat(analysis/convex/extreme): extreme sets (#7357) define extreme sets

Estimated changes

Modified docs/references.bib

Modified src/analysis/convex/basic.lean

added theorem convex.convex_remove_iff_not_mem_convex_hull_remove

added theorem convex.open_segment_subset

modified theorem convex.segment_subset

added theorem convex_iff_open_segment_subset

modified theorem convex_iff_segment_subset

added theorem left_mem_open_segment_iff

added theorem mem_open_segment_of_ne_left_right

added theorem mem_open_segment_translate

added def open_segment

added theorem open_segment_eq_Ioo'

added theorem open_segment_eq_Ioo

added theorem open_segment_eq_image'

added theorem open_segment_eq_image

added theorem open_segment_eq_image₂

added theorem open_segment_image

added theorem open_segment_same

added theorem open_segment_subset_segment

added theorem open_segment_symm

added theorem open_segment_translate_image

added theorem open_segment_translate_preimage

added theorem right_mem_open_segment_iff

modified theorem segment_eq_image'

modified theorem segment_eq_image

modified theorem segment_translate_image

Created src/analysis/convex/extreme.lean

added theorem convex.mem_extreme_points_iff_convex_remove

added theorem convex.mem_extreme_points_iff_mem_diff_convex_hull_remove

added theorem extreme_points_convex_hull_subset

added theorem extreme_points_def

added theorem extreme_points_empty

added theorem extreme_points_singleton

added theorem extreme_points_subset

added theorem inter_extreme_points_subset_extreme_points_of_subset

added theorem is_extreme.Inter

added theorem is_extreme.antisymm

added theorem is_extreme.bInter

added theorem is_extreme.convex_diff

added theorem is_extreme.extreme_points_eq

added theorem is_extreme.extreme_points_subset_extreme_points

added theorem is_extreme.inter

added theorem is_extreme.mono

added theorem is_extreme.refl

added theorem is_extreme.sInter

added theorem is_extreme.trans

added def is_extreme

added theorem mem_extreme_points_iff_extreme_singleton

added theorem mem_extreme_points_iff_forall_segment

added def set.extreme_points

Modified src/data/set/intervals/image_preimage.lean

added theorem set.image_mul_left_Ioo

added theorem set.image_mul_right_Ioo