Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-12 16:16 357b2966

View on Github →

feat(analysis/convex/side): betweenness and affine subspaces (#16733) Define notions of points being (weakly or strictly) on the same side or opposite sides of an affine subspace (e.g. a line), for use in describing geometrical configurations, and provide some associated API.

Estimated changes

Created src/analysis/convex/side.lean

added theorem affine_equiv.s_opp_side_map_iff

added theorem affine_equiv.s_same_side_map_iff

added theorem affine_equiv.w_opp_side_map_iff

added theorem affine_equiv.w_same_side_map_iff

added theorem affine_subspace.not_s_opp_side_bot

added theorem affine_subspace.not_s_opp_side_self

added theorem affine_subspace.not_s_same_side_bot

added theorem affine_subspace.not_w_opp_side_bot

added theorem affine_subspace.not_w_same_side_bot

added theorem affine_subspace.s_opp_side.exists_sbtw

added theorem affine_subspace.s_opp_side.left_not_mem

added theorem affine_subspace.s_opp_side.nonempty

added theorem affine_subspace.s_opp_side.not_s_same_side

added theorem affine_subspace.s_opp_side.not_w_same_side

added theorem affine_subspace.s_opp_side.right_not_mem

added theorem affine_subspace.s_opp_side.trans

added theorem affine_subspace.s_opp_side.trans_s_same_side

added theorem affine_subspace.s_opp_side.trans_w_opp_side

added theorem affine_subspace.s_opp_side.trans_w_same_side

added theorem affine_subspace.s_opp_side.w_opp_side

added def affine_subspace.s_opp_side

added theorem affine_subspace.s_opp_side_comm

added theorem affine_subspace.s_opp_side_iff_exists_left

added theorem affine_subspace.s_opp_side_iff_exists_right

added theorem affine_subspace.s_opp_side_line_map_left

added theorem affine_subspace.s_opp_side_line_map_right

added theorem affine_subspace.s_opp_side_smul_vsub_vadd_left

added theorem affine_subspace.s_opp_side_smul_vsub_vadd_right

added theorem affine_subspace.s_opp_side_vadd_left_iff

added theorem affine_subspace.s_opp_side_vadd_right_iff

added theorem affine_subspace.s_same_side.left_not_mem

added theorem affine_subspace.s_same_side.nonempty

added theorem affine_subspace.s_same_side.not_s_opp_side

added theorem affine_subspace.s_same_side.not_w_opp_side

added theorem affine_subspace.s_same_side.right_not_mem

added theorem affine_subspace.s_same_side.trans

added theorem affine_subspace.s_same_side.trans_s_opp_side

added theorem affine_subspace.s_same_side.trans_w_opp_side

added theorem affine_subspace.s_same_side.trans_w_same_side

added theorem affine_subspace.s_same_side.w_same_side

added def affine_subspace.s_same_side

added theorem affine_subspace.s_same_side_comm

added theorem affine_subspace.s_same_side_iff_exists_left

added theorem affine_subspace.s_same_side_iff_exists_right

added theorem affine_subspace.s_same_side_line_map_left

added theorem affine_subspace.s_same_side_line_map_right

added theorem affine_subspace.s_same_side_self_iff

added theorem affine_subspace.s_same_side_smul_vsub_vadd_left

added theorem affine_subspace.s_same_side_smul_vsub_vadd_right

added theorem affine_subspace.s_same_side_vadd_left_iff

added theorem affine_subspace.s_same_side_vadd_right_iff

added theorem affine_subspace.set_of_s_opp_side_eq_image2

added theorem affine_subspace.set_of_s_same_side_eq_image2

added theorem affine_subspace.set_of_w_opp_side_eq_image2

added theorem affine_subspace.set_of_w_same_side_eq_image2

added theorem affine_subspace.w_opp_side.map

added theorem affine_subspace.w_opp_side.nonempty

added theorem affine_subspace.w_opp_side.not_s_same_side

added theorem affine_subspace.w_opp_side.trans

added theorem affine_subspace.w_opp_side.trans_s_opp_side

added theorem affine_subspace.w_opp_side.trans_s_same_side

added theorem affine_subspace.w_opp_side.trans_w_same_side

added def affine_subspace.w_opp_side

added theorem affine_subspace.w_opp_side_comm

added theorem affine_subspace.w_opp_side_iff_exists_left

added theorem affine_subspace.w_opp_side_iff_exists_right

added theorem affine_subspace.w_opp_side_iff_exists_wbtw

added theorem affine_subspace.w_opp_side_line_map_left

added theorem affine_subspace.w_opp_side_line_map_right

added theorem affine_subspace.w_opp_side_of_left_mem

added theorem affine_subspace.w_opp_side_of_right_mem

added theorem affine_subspace.w_opp_side_self_iff

added theorem affine_subspace.w_opp_side_smul_vsub_vadd_left

added theorem affine_subspace.w_opp_side_smul_vsub_vadd_right

added theorem affine_subspace.w_opp_side_vadd_left_iff

added theorem affine_subspace.w_opp_side_vadd_right_iff

added theorem affine_subspace.w_same_side.map

added theorem affine_subspace.w_same_side.nonempty

added theorem affine_subspace.w_same_side.not_s_opp_side

added theorem affine_subspace.w_same_side.trans

added theorem affine_subspace.w_same_side.trans_s_opp_side

added theorem affine_subspace.w_same_side.trans_s_same_side

added theorem affine_subspace.w_same_side.trans_w_opp_side

added def affine_subspace.w_same_side

added theorem affine_subspace.w_same_side_and_w_opp_side_iff

added theorem affine_subspace.w_same_side_comm

added theorem affine_subspace.w_same_side_iff_exists_left

added theorem affine_subspace.w_same_side_iff_exists_right

added theorem affine_subspace.w_same_side_line_map_left

added theorem affine_subspace.w_same_side_line_map_right

added theorem affine_subspace.w_same_side_of_left_mem

added theorem affine_subspace.w_same_side_of_right_mem

added theorem affine_subspace.w_same_side_self_iff

added theorem affine_subspace.w_same_side_smul_vsub_vadd_left

added theorem affine_subspace.w_same_side_smul_vsub_vadd_right

added theorem affine_subspace.w_same_side_vadd_left_iff

added theorem affine_subspace.w_same_side_vadd_right_iff

added theorem function.injective.s_opp_side_map_iff

added theorem function.injective.s_same_side_map_iff

added theorem function.injective.w_opp_side_map_iff

added theorem function.injective.w_same_side_map_iff

added theorem sbtw.s_opp_side_of_not_mem_of_mem

added theorem wbtw.w_opp_side₁₃

added theorem wbtw.w_opp_side₃₁

added theorem wbtw.w_same_side₁₂

added theorem wbtw.w_same_side₂₁

added theorem wbtw.w_same_side₂₃

added theorem wbtw.w_same_side₃₂