Commit 2023-05-22 12:09 9247bc46

View on Github →

feat: port Analysis.Convex.Between (#3790)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Between.lean

added theorem AffineEquiv.sbtw_map_iff

added theorem AffineEquiv.wbtw_map_iff

added theorem Collinear.wbtw_or_wbtw_or_wbtw

added theorem Function.Injective.sbtw_map_iff

added theorem Function.Injective.wbtw_map_iff

added theorem Sbtw.affineCombination_of_mem_affineSpan_pair

added theorem Sbtw.left_mem_affineSpan

added theorem Sbtw.left_mem_image_Ioi

added theorem Sbtw.left_ne

added theorem Sbtw.left_ne_right

added theorem Sbtw.mem_image_Ioo

added theorem Sbtw.ne_left

added theorem Sbtw.ne_right

added theorem Sbtw.not_rotate

added theorem Sbtw.not_swap_left

added theorem Sbtw.not_swap_right

added theorem Sbtw.right_mem_affineSpan

added theorem Sbtw.right_mem_image_Ioi

added theorem Sbtw.right_ne

added theorem Sbtw.trans_left

added theorem Sbtw.trans_left_right

added theorem Sbtw.trans_right

added theorem Sbtw.trans_right_left

added theorem Sbtw.trans_wbtw_left_ne

added theorem Sbtw.trans_wbtw_right_ne

added theorem Sbtw.wbtw

added def Sbtw

added theorem Wbtw.collinear

added theorem Wbtw.left_mem_affineSpan_of_right_ne

added theorem Wbtw.left_mem_image_Ici_of_right_ne

added theorem Wbtw.left_ne_right_of_ne_left

added theorem Wbtw.left_ne_right_of_ne_right

added theorem Wbtw.map

added theorem Wbtw.mem_affineSpan

added theorem Wbtw.right_mem_affineSpan_of_left_ne

added theorem Wbtw.right_mem_image_Ici_of_left_ne

added theorem Wbtw.rotate_iff

added theorem Wbtw.sameRay_vsub

added theorem Wbtw.sameRay_vsub_left

added theorem Wbtw.sameRay_vsub_right

added theorem Wbtw.swap_left_iff

added theorem Wbtw.swap_right_iff

added theorem Wbtw.trans_left

added theorem Wbtw.trans_left_ne

added theorem Wbtw.trans_left_right

added theorem Wbtw.trans_right

added theorem Wbtw.trans_right_left

added theorem Wbtw.trans_right_ne

added theorem Wbtw.trans_sbtw_left

added theorem Wbtw.trans_sbtw_right

added def Wbtw

added def affineSegment

added theorem affineSegment_comm

added theorem affineSegment_const_vadd_image

added theorem affineSegment_const_vsub_image

added theorem affineSegment_eq_segment

added theorem affineSegment_image

added theorem affineSegment_vadd_const_image

added theorem affineSegment_vsub_const_image

added theorem left_mem_affineSegment

added theorem mem_const_vadd_affineSegment

added theorem mem_const_vsub_affineSegment

added theorem mem_vadd_const_affineSegment

added theorem mem_vsub_const_affineSegment

added theorem not_sbtw_self

added theorem not_sbtw_self_left

added theorem not_sbtw_self_right

added theorem right_mem_affineSegment

added theorem sbtw_comm

added theorem sbtw_const_vadd_iff

added theorem sbtw_const_vsub_iff

added theorem sbtw_iff_left_ne_and_right_mem_image_Ioi

added theorem sbtw_iff_mem_image_Ioo_and_ne

added theorem sbtw_iff_right_ne_and_left_mem_image_Ioi

added theorem sbtw_lineMap_iff

added theorem sbtw_midpoint_of_ne

added theorem sbtw_mul_sub_add_iff

added theorem sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair

added theorem sbtw_one_zero_iff

added theorem sbtw_pointReflection_of_ne

added theorem sbtw_vadd_const_iff

added theorem sbtw_vsub_const_iff

added theorem sbtw_zero_one_iff

added theorem wbtw_comm

added theorem wbtw_const_vadd_iff

added theorem wbtw_const_vsub_iff

added theorem wbtw_iff_left_eq_or_right_mem_image_Ici

added theorem wbtw_iff_right_eq_or_left_mem_image_Ici

added theorem wbtw_iff_sameRay_vsub

added theorem wbtw_lineMap_iff

added theorem wbtw_midpoint

added theorem wbtw_mul_sub_add_iff

added theorem wbtw_one_zero_iff

added theorem wbtw_or_wbtw_smul_vadd_of_nonneg

added theorem wbtw_or_wbtw_smul_vadd_of_nonpos

added theorem wbtw_pointReflection

added theorem wbtw_rotate_iff

added theorem wbtw_self_iff

added theorem wbtw_self_left

added theorem wbtw_self_right

added theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_le

added theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos

added theorem wbtw_smul_vadd_smul_vadd_of_nonpos_of_le

added theorem wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg

added theorem wbtw_swap_left_iff

added theorem wbtw_swap_right_iff

added theorem wbtw_vadd_const_iff

added theorem wbtw_vsub_const_iff

added theorem wbtw_zero_one_iff

Modified Mathlib/Data/Set/Pointwise/SMul.lean