Commit 2023-03-24 15:22 4e301f43

View on Github →

feat: port Analysis.Convex.Segment (#2869)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Segment.lean

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 Icc_subset_segment

added theorem Ioo_subset_openSegment

added theorem Pi.image_update_openSegment

added theorem Pi.image_update_segment

added theorem Pi.openSegment_subset

added theorem Pi.segment_subset

added theorem Prod.image_mk_openSegment_left

added theorem Prod.image_mk_openSegment_right

added theorem Prod.image_mk_segment_left

added theorem Prod.image_mk_segment_right

added theorem Prod.openSegment_subset

added theorem Prod.segment_subset

added theorem image_openSegment

added theorem image_segment

added theorem insert_endpoints_openSegment

added theorem left_mem_openSegment_iff

added theorem left_mem_segment

added theorem mem_openSegment_iff_div

added theorem mem_openSegment_of_ne_left_right

added theorem mem_openSegment_translate

added theorem mem_segment_add_sub

added theorem mem_segment_iff_div

added theorem mem_segment_iff_sameRay

added theorem mem_segment_sub_add

added theorem mem_segment_translate

added theorem midpoint_mem_segment

added def openSegment

added theorem openSegment_eq_Ioo'

added theorem openSegment_eq_Ioo

added theorem openSegment_eq_image'

added theorem openSegment_eq_image

added theorem openSegment_eq_image_lineMap

added theorem openSegment_eq_image₂

added theorem openSegment_same

added theorem openSegment_subset_Ioo

added theorem openSegment_subset_iff

added theorem openSegment_subset_iff_segment_subset

added theorem openSegment_subset_segment

added theorem openSegment_subset_union

added theorem openSegment_symm

added theorem openSegment_translate_image

added theorem openSegment_translate_preimage

added theorem right_mem_openSegment_iff

added theorem right_mem_segment

added theorem sameRay_of_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_lineMap

added theorem segment_eq_image₂

added theorem segment_eq_uIcc

added theorem segment_same

added theorem segment_subset_Icc

added theorem segment_subset_iff

added theorem segment_subset_uIcc

added theorem segment_symm

added theorem segment_translate_image

added theorem segment_translate_preimage

added theorem vadd_openSegment

added theorem vadd_segment