Commit 2023-05-23 07:30 32b9ea8c

View on Github →

feat: port Analysis.Convex.Side (#4250)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Side.lean

added theorem AffineEquiv.sOppSide_map_iff

added theorem AffineEquiv.sSameSide_map_iff

added theorem AffineEquiv.wOppSide_map_iff

added theorem AffineEquiv.wSameSide_map_iff

added theorem AffineSubspace.SOppSide.exists_sbtw

added theorem AffineSubspace.SOppSide.left_not_mem

added theorem AffineSubspace.SOppSide.nonempty

added theorem AffineSubspace.SOppSide.not_sSameSide

added theorem AffineSubspace.SOppSide.not_wSameSide

added theorem AffineSubspace.SOppSide.right_not_mem

added theorem AffineSubspace.SOppSide.trans

added theorem AffineSubspace.SOppSide.trans_sSameSide

added theorem AffineSubspace.SOppSide.trans_wOppSide

added theorem AffineSubspace.SOppSide.trans_wSameSide

added theorem AffineSubspace.SOppSide.wOppSide

added def AffineSubspace.SOppSide

added theorem AffineSubspace.SSameSide.left_not_mem

added theorem AffineSubspace.SSameSide.nonempty

added theorem AffineSubspace.SSameSide.not_sOppSide

added theorem AffineSubspace.SSameSide.not_wOppSide

added theorem AffineSubspace.SSameSide.right_not_mem

added theorem AffineSubspace.SSameSide.trans

added theorem AffineSubspace.SSameSide.trans_sOppSide

added theorem AffineSubspace.SSameSide.trans_wOppSide

added theorem AffineSubspace.SSameSide.trans_wSameSide

added theorem AffineSubspace.SSameSide.wSameSide

added def AffineSubspace.SSameSide

added theorem AffineSubspace.WOppSide.map

added theorem AffineSubspace.WOppSide.nonempty

added theorem AffineSubspace.WOppSide.not_sSameSide

added theorem AffineSubspace.WOppSide.trans

added theorem AffineSubspace.WOppSide.trans_sOppSide

added theorem AffineSubspace.WOppSide.trans_sSameSide

added theorem AffineSubspace.WOppSide.trans_wSameSide

added def AffineSubspace.WOppSide

added theorem AffineSubspace.WSameSide.map

added theorem AffineSubspace.WSameSide.nonempty

added theorem AffineSubspace.WSameSide.not_sOppSide

added theorem AffineSubspace.WSameSide.trans

added theorem AffineSubspace.WSameSide.trans_sOppSide

added theorem AffineSubspace.WSameSide.trans_sSameSide

added theorem AffineSubspace.WSameSide.trans_wOppSide

added def AffineSubspace.WSameSide

added theorem AffineSubspace.isConnected_setOf_sOppSide

added theorem AffineSubspace.isConnected_setOf_sSameSide

added theorem AffineSubspace.isConnected_setOf_wOppSide

added theorem AffineSubspace.isConnected_setOf_wSameSide

added theorem AffineSubspace.isPreconnected_setOf_sOppSide

added theorem AffineSubspace.isPreconnected_setOf_sSameSide

added theorem AffineSubspace.isPreconnected_setOf_wOppSide

added theorem AffineSubspace.isPreconnected_setOf_wSameSide

added theorem AffineSubspace.not_sOppSide_bot

added theorem AffineSubspace.not_sOppSide_self

added theorem AffineSubspace.not_sSameSide_bot

added theorem AffineSubspace.not_wOppSide_bot

added theorem AffineSubspace.not_wSameSide_bot

added theorem AffineSubspace.sOppSide_comm

added theorem AffineSubspace.sOppSide_iff_exists_left

added theorem AffineSubspace.sOppSide_iff_exists_right

added theorem AffineSubspace.sOppSide_lineMap_left

added theorem AffineSubspace.sOppSide_lineMap_right

added theorem AffineSubspace.sOppSide_pointReflection

added theorem AffineSubspace.sOppSide_smul_vsub_vadd_left

added theorem AffineSubspace.sOppSide_smul_vsub_vadd_right

added theorem AffineSubspace.sOppSide_vadd_left_iff

added theorem AffineSubspace.sOppSide_vadd_right_iff

added theorem AffineSubspace.sSameSide_comm

added theorem AffineSubspace.sSameSide_iff_exists_left

added theorem AffineSubspace.sSameSide_iff_exists_right

added theorem AffineSubspace.sSameSide_lineMap_left

added theorem AffineSubspace.sSameSide_lineMap_right

added theorem AffineSubspace.sSameSide_self_iff

added theorem AffineSubspace.sSameSide_smul_vsub_vadd_left

added theorem AffineSubspace.sSameSide_smul_vsub_vadd_right

added theorem AffineSubspace.sSameSide_vadd_left_iff

added theorem AffineSubspace.sSameSide_vadd_right_iff

added theorem AffineSubspace.setOf_sOppSide_eq_image2

added theorem AffineSubspace.setOf_sSameSide_eq_image2

added theorem AffineSubspace.setOf_wOppSide_eq_image2

added theorem AffineSubspace.setOf_wSameSide_eq_image2

added theorem AffineSubspace.wOppSide_comm

added theorem AffineSubspace.wOppSide_iff_exists_left

added theorem AffineSubspace.wOppSide_iff_exists_right

added theorem AffineSubspace.wOppSide_iff_exists_wbtw

added theorem AffineSubspace.wOppSide_lineMap_left

added theorem AffineSubspace.wOppSide_lineMap_right

added theorem AffineSubspace.wOppSide_of_left_mem

added theorem AffineSubspace.wOppSide_of_right_mem

added theorem AffineSubspace.wOppSide_pointReflection

added theorem AffineSubspace.wOppSide_self_iff

added theorem AffineSubspace.wOppSide_smul_vsub_vadd_left

added theorem AffineSubspace.wOppSide_smul_vsub_vadd_right

added theorem AffineSubspace.wOppSide_vadd_left_iff

added theorem AffineSubspace.wOppSide_vadd_right_iff

added theorem AffineSubspace.wSameSide_and_wOppSide_iff

added theorem AffineSubspace.wSameSide_comm

added theorem AffineSubspace.wSameSide_iff_exists_left

added theorem AffineSubspace.wSameSide_iff_exists_right

added theorem AffineSubspace.wSameSide_lineMap_left

added theorem AffineSubspace.wSameSide_lineMap_right

added theorem AffineSubspace.wSameSide_of_left_mem

added theorem AffineSubspace.wSameSide_of_right_mem

added theorem AffineSubspace.wSameSide_self_iff

added theorem AffineSubspace.wSameSide_smul_vsub_vadd_left

added theorem AffineSubspace.wSameSide_smul_vsub_vadd_right

added theorem AffineSubspace.wSameSide_vadd_left_iff

added theorem AffineSubspace.wSameSide_vadd_right_iff

added theorem Function.Injective.sOppSide_map_iff

added theorem Function.Injective.sSameSide_map_iff

added theorem Function.Injective.wOppSide_map_iff

added theorem Function.Injective.wSameSide_map_iff

added theorem Sbtw.sOppSide_of_not_mem_of_mem

added theorem Wbtw.wOppSide₁₃

added theorem Wbtw.wOppSide₃₁

added theorem Wbtw.wSameSide₁₂

added theorem Wbtw.wSameSide₂₁

added theorem Wbtw.wSameSide₂₃

added theorem Wbtw.wSameSide₃₂