Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-20 08:58 4705dd0d

View on Github →

split(analysis/convex/segment): Split off analysis/convex.basic (#16112) Move segment and open_segment to a new file analysis.convex.segment.

Estimated changes

deleted theorem Icc_subset_segment
deleted theorem Ioo_subset_open_segment
deleted theorem convex.combo_le_max
deleted theorem convex.mem_Icc
deleted theorem convex.mem_Ico
deleted theorem convex.mem_Ioc
deleted theorem convex.mem_Ioo
deleted theorem convex.min_le_combo
deleted theorem left_mem_open_segment_iff
deleted theorem left_mem_segment
deleted theorem mem_open_segment_iff_div
deleted theorem mem_segment_add_sub
deleted theorem mem_segment_iff_div
deleted theorem mem_segment_iff_same_ray
deleted theorem mem_segment_sub_add
deleted theorem mem_segment_translate
deleted theorem midpoint_mem_segment
deleted def open_segment
deleted theorem open_segment_eq_Ioo'
deleted theorem open_segment_eq_Ioo
deleted theorem open_segment_eq_image'
deleted theorem open_segment_eq_image
deleted theorem open_segment_eq_image₂
deleted theorem open_segment_image
deleted theorem open_segment_same
deleted theorem open_segment_subset_Ioo
deleted theorem open_segment_subset_iff
deleted theorem open_segment_symm
deleted theorem right_mem_segment
deleted theorem same_ray_of_mem_segment
deleted def segment
deleted theorem segment_eq_Icc'
deleted theorem segment_eq_Icc
deleted theorem segment_eq_image'
deleted theorem segment_eq_image
deleted theorem segment_eq_image_line_map
deleted theorem segment_eq_image₂
deleted theorem segment_eq_interval
deleted theorem segment_image
deleted theorem segment_same
deleted theorem segment_subset_Icc
deleted theorem segment_subset_iff
deleted theorem segment_subset_interval
deleted theorem segment_symm
deleted theorem segment_translate_image
added theorem Icc_subset_segment
added theorem convex.combo_le_max
added theorem convex.mem_Icc
added theorem convex.mem_Ico
added theorem convex.mem_Ioc
added theorem convex.mem_Ioo
added theorem convex.min_le_combo
added theorem left_mem_segment
added theorem mem_segment_add_sub
added theorem mem_segment_iff_div
added theorem mem_segment_sub_add
added theorem mem_segment_translate
added theorem midpoint_mem_segment
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_image
added theorem open_segment_same
added theorem open_segment_symm
added theorem right_mem_segment
added def segment
added theorem segment_eq_Icc'
added theorem segment_eq_Icc
added theorem segment_eq_image'
added theorem segment_eq_image
added theorem segment_eq_image₂
added theorem segment_eq_interval
added theorem segment_image
added theorem segment_same
added theorem segment_subset_Icc
added theorem segment_subset_iff
added theorem segment_symm