Sides of affine subspaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines notions of two points being on the same or opposite sides of an affine subspace.
Main definitions #
s.w_same_side x y: The pointsxandyare weakly on the same side of the affine subspaces.s.s_same_side x y: The pointsxandyare strictly on the same side of the affine subspaces.s.w_opp_side x y: The pointsxandyare weakly on opposite sides of the affine subspaces.s.s_opp_side x y: The pointsxandyare strictly on opposite sides of the affine subspaces.
def
affine_subspace.w_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(s : affine_subspace R P)
(x y : P) :
Prop
The points x and y are weakly on the same side of s.
def
affine_subspace.s_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(s : affine_subspace R P)
(x y : P) :
Prop
The points x and y are strictly on the same side of s.
Equations
- s.s_same_side x y = (s.w_same_side x y ∧ x ∉ s ∧ y ∉ s)
def
affine_subspace.w_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(s : affine_subspace R P)
(x y : P) :
Prop
The points x and y are weakly on opposite sides of s.
def
affine_subspace.s_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(s : affine_subspace R P)
(x y : P) :
Prop
The points x and y are strictly on opposite sides of s.
Equations
- s.s_opp_side x y = (s.w_opp_side x y ∧ x ∉ s ∧ y ∉ s)
theorem
affine_subspace.w_same_side.map
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
(h : s.w_same_side x y)
(f : P →ᵃ[R] P') :
(affine_subspace.map f s).w_same_side (⇑f x) (⇑f y)
theorem
function.injective.w_same_side_map_iff
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
{f : P →ᵃ[R] P'}
(hf : function.injective ⇑f) :
(affine_subspace.map f s).w_same_side (⇑f x) (⇑f y) ↔ s.w_same_side x y
theorem
function.injective.s_same_side_map_iff
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
{f : P →ᵃ[R] P'}
(hf : function.injective ⇑f) :
(affine_subspace.map f s).s_same_side (⇑f x) (⇑f y) ↔ s.s_same_side x y
@[simp]
theorem
affine_equiv.w_same_side_map_iff
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
(f : P ≃ᵃ[R] P') :
(affine_subspace.map ↑f s).w_same_side (⇑f x) (⇑f y) ↔ s.w_same_side x y
@[simp]
theorem
affine_equiv.s_same_side_map_iff
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
(f : P ≃ᵃ[R] P') :
(affine_subspace.map ↑f s).s_same_side (⇑f x) (⇑f y) ↔ s.s_same_side x y
theorem
affine_subspace.w_opp_side.map
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
(h : s.w_opp_side x y)
(f : P →ᵃ[R] P') :
(affine_subspace.map f s).w_opp_side (⇑f x) (⇑f y)
theorem
function.injective.w_opp_side_map_iff
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
{f : P →ᵃ[R] P'}
(hf : function.injective ⇑f) :
(affine_subspace.map f s).w_opp_side (⇑f x) (⇑f y) ↔ s.w_opp_side x y
theorem
function.injective.s_opp_side_map_iff
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
{f : P →ᵃ[R] P'}
(hf : function.injective ⇑f) :
(affine_subspace.map f s).s_opp_side (⇑f x) (⇑f y) ↔ s.s_opp_side x y
@[simp]
theorem
affine_equiv.w_opp_side_map_iff
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
(f : P ≃ᵃ[R] P') :
(affine_subspace.map ↑f s).w_opp_side (⇑f x) (⇑f y) ↔ s.w_opp_side x y
@[simp]
theorem
affine_equiv.s_opp_side_map_iff
{R : Type u_1}
{V : Type u_2}
{V' : Type u_3}
{P : Type u_4}
{P' : Type u_5}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
[add_comm_group V']
[module R V']
[add_torsor V' P']
{s : affine_subspace R P}
{x y : P}
(f : P ≃ᵃ[R] P') :
(affine_subspace.map ↑f s).s_opp_side (⇑f x) (⇑f y) ↔ s.s_opp_side x y
theorem
affine_subspace.w_same_side.nonempty
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.w_same_side x y) :
theorem
affine_subspace.s_same_side.nonempty
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_same_side x y) :
theorem
affine_subspace.w_opp_side.nonempty
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.w_opp_side x y) :
theorem
affine_subspace.s_opp_side.nonempty
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_opp_side x y) :
theorem
affine_subspace.s_same_side.w_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_same_side x y) :
s.w_same_side x y
theorem
affine_subspace.s_same_side.left_not_mem
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_same_side x y) :
x ∉ s
theorem
affine_subspace.s_same_side.right_not_mem
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_same_side x y) :
y ∉ s
theorem
affine_subspace.s_opp_side.w_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_opp_side x y) :
s.w_opp_side x y
theorem
affine_subspace.s_opp_side.left_not_mem
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_opp_side x y) :
x ∉ s
theorem
affine_subspace.s_opp_side.right_not_mem
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_opp_side x y) :
y ∉ s
theorem
affine_subspace.w_same_side_comm
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
s.w_same_side x y ↔ s.w_same_side y x
theorem
affine_subspace.w_same_side.symm
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
s.w_same_side x y → s.w_same_side y x
Alias of the forward direction of affine_subspace.w_same_side_comm.
theorem
affine_subspace.s_same_side_comm
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
s.s_same_side x y ↔ s.s_same_side y x
theorem
affine_subspace.s_same_side.symm
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
s.s_same_side x y → s.s_same_side y x
Alias of the forward direction of affine_subspace.s_same_side_comm.
theorem
affine_subspace.w_opp_side_comm
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
s.w_opp_side x y ↔ s.w_opp_side y x
theorem
affine_subspace.w_opp_side.symm
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
s.w_opp_side x y → s.w_opp_side y x
Alias of the forward direction of affine_subspace.w_opp_side_comm.
theorem
affine_subspace.s_opp_side_comm
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
s.s_opp_side x y ↔ s.s_opp_side y x
theorem
affine_subspace.s_opp_side.symm
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
s.s_opp_side x y → s.s_opp_side y x
Alias of the forward direction of affine_subspace.s_opp_side_comm.
theorem
affine_subspace.not_w_same_side_bot
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(x y : P) :
¬⊥.w_same_side x y
theorem
affine_subspace.not_s_same_side_bot
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(x y : P) :
¬⊥.s_same_side x y
theorem
affine_subspace.not_w_opp_side_bot
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(x y : P) :
¬⊥.w_opp_side x y
theorem
affine_subspace.not_s_opp_side_bot
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(x y : P) :
¬⊥.s_opp_side x y
@[simp]
theorem
affine_subspace.w_same_side_self_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P} :
s.w_same_side x x ↔ ↑s.nonempty
theorem
affine_subspace.s_same_side_self_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P} :
theorem
affine_subspace.w_same_side_of_left_mem
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P}
(y : P)
(hx : x ∈ s) :
s.w_same_side x y
theorem
affine_subspace.w_same_side_of_right_mem
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
(x : P)
{y : P}
(hy : y ∈ s) :
s.w_same_side x y
theorem
affine_subspace.w_opp_side_of_left_mem
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P}
(y : P)
(hx : x ∈ s) :
s.w_opp_side x y
theorem
affine_subspace.w_opp_side_of_right_mem
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
(x : P)
{y : P}
(hy : y ∈ s) :
s.w_opp_side x y
theorem
affine_subspace.w_same_side_vadd_left_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
{v : V}
(hv : v ∈ s.direction) :
s.w_same_side (v +ᵥ x) y ↔ s.w_same_side x y
theorem
affine_subspace.w_same_side_vadd_right_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
{v : V}
(hv : v ∈ s.direction) :
s.w_same_side x (v +ᵥ y) ↔ s.w_same_side x y
theorem
affine_subspace.s_same_side_vadd_left_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
{v : V}
(hv : v ∈ s.direction) :
s.s_same_side (v +ᵥ x) y ↔ s.s_same_side x y
theorem
affine_subspace.s_same_side_vadd_right_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
{v : V}
(hv : v ∈ s.direction) :
s.s_same_side x (v +ᵥ y) ↔ s.s_same_side x y
theorem
affine_subspace.w_opp_side_vadd_left_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
{v : V}
(hv : v ∈ s.direction) :
s.w_opp_side (v +ᵥ x) y ↔ s.w_opp_side x y
theorem
affine_subspace.w_opp_side_vadd_right_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
{v : V}
(hv : v ∈ s.direction) :
s.w_opp_side x (v +ᵥ y) ↔ s.w_opp_side x y
theorem
affine_subspace.s_opp_side_vadd_left_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
{v : V}
(hv : v ∈ s.direction) :
s.s_opp_side (v +ᵥ x) y ↔ s.s_opp_side x y
theorem
affine_subspace.s_opp_side_vadd_right_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
{v : V}
(hv : v ∈ s.direction) :
s.s_opp_side x (v +ᵥ y) ↔ s.s_opp_side x y
theorem
affine_subspace.w_same_side_smul_vsub_vadd_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{p₁ p₂ : P}
(x : P)
(hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s)
{t : R}
(ht : 0 ≤ t) :
s.w_same_side (t • (x -ᵥ p₁) +ᵥ p₂) x
theorem
affine_subspace.w_same_side_smul_vsub_vadd_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{p₁ p₂ : P}
(x : P)
(hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s)
{t : R}
(ht : 0 ≤ t) :
s.w_same_side x (t • (x -ᵥ p₁) +ᵥ p₂)
theorem
affine_subspace.w_same_side_line_map_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P}
(y : P)
(h : x ∈ s)
{t : R}
(ht : 0 ≤ t) :
s.w_same_side (⇑(affine_map.line_map x y) t) y
theorem
affine_subspace.w_same_side_line_map_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P}
(y : P)
(h : x ∈ s)
{t : R}
(ht : 0 ≤ t) :
s.w_same_side y (⇑(affine_map.line_map x y) t)
theorem
affine_subspace.w_opp_side_smul_vsub_vadd_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{p₁ p₂ : P}
(x : P)
(hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s)
{t : R}
(ht : t ≤ 0) :
s.w_opp_side (t • (x -ᵥ p₁) +ᵥ p₂) x
theorem
affine_subspace.w_opp_side_smul_vsub_vadd_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{p₁ p₂ : P}
(x : P)
(hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s)
{t : R}
(ht : t ≤ 0) :
s.w_opp_side x (t • (x -ᵥ p₁) +ᵥ p₂)
theorem
affine_subspace.w_opp_side_line_map_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P}
(y : P)
(h : x ∈ s)
{t : R}
(ht : t ≤ 0) :
s.w_opp_side (⇑(affine_map.line_map x y) t) y
theorem
affine_subspace.w_opp_side_line_map_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P}
(y : P)
(h : x ∈ s)
{t : R}
(ht : t ≤ 0) :
s.w_opp_side y (⇑(affine_map.line_map x y) t)
theorem
wbtw.w_same_side₂₃
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(h : wbtw R x y z)
(hx : x ∈ s) :
s.w_same_side y z
theorem
wbtw.w_same_side₃₂
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(h : wbtw R x y z)
(hx : x ∈ s) :
s.w_same_side z y
theorem
wbtw.w_same_side₁₂
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(h : wbtw R x y z)
(hz : z ∈ s) :
s.w_same_side x y
theorem
wbtw.w_same_side₂₁
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(h : wbtw R x y z)
(hz : z ∈ s) :
s.w_same_side y x
theorem
wbtw.w_opp_side₁₃
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(h : wbtw R x y z)
(hy : y ∈ s) :
s.w_opp_side x z
theorem
wbtw.w_opp_side₃₁
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[strict_ordered_comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(h : wbtw R x y z)
(hy : y ∈ s) :
s.w_opp_side z x
@[simp]
theorem
affine_subspace.w_opp_side_self_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P} :
s.w_opp_side x x ↔ x ∈ s
theorem
affine_subspace.not_s_opp_side_self
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(s : affine_subspace R P)
(x : P) :
¬s.s_opp_side x x
theorem
affine_subspace.w_same_side_iff_exists_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y p₁ : P}
(h : p₁ ∈ s) :
theorem
affine_subspace.w_same_side_iff_exists_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y p₂ : P}
(h : p₂ ∈ s) :
theorem
affine_subspace.s_same_side_iff_exists_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y p₁ : P}
(h : p₁ ∈ s) :
theorem
affine_subspace.s_same_side_iff_exists_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y p₂ : P}
(h : p₂ ∈ s) :
theorem
affine_subspace.w_opp_side_iff_exists_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y p₁ : P}
(h : p₁ ∈ s) :
theorem
affine_subspace.w_opp_side_iff_exists_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y p₂ : P}
(h : p₂ ∈ s) :
theorem
affine_subspace.s_opp_side_iff_exists_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y p₁ : P}
(h : p₁ ∈ s) :
theorem
affine_subspace.s_opp_side_iff_exists_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y p₂ : P}
(h : p₂ ∈ s) :
theorem
affine_subspace.w_same_side.trans
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.w_same_side x y)
(hyz : s.w_same_side y z)
(hy : y ∉ s) :
s.w_same_side x z
theorem
affine_subspace.w_same_side.trans_s_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.w_same_side x y)
(hyz : s.s_same_side y z) :
s.w_same_side x z
theorem
affine_subspace.w_same_side.trans_w_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.w_same_side x y)
(hyz : s.w_opp_side y z)
(hy : y ∉ s) :
s.w_opp_side x z
theorem
affine_subspace.w_same_side.trans_s_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.w_same_side x y)
(hyz : s.s_opp_side y z) :
s.w_opp_side x z
theorem
affine_subspace.s_same_side.trans_w_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.s_same_side x y)
(hyz : s.w_same_side y z) :
s.w_same_side x z
theorem
affine_subspace.s_same_side.trans
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.s_same_side x y)
(hyz : s.s_same_side y z) :
s.s_same_side x z
theorem
affine_subspace.s_same_side.trans_w_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.s_same_side x y)
(hyz : s.w_opp_side y z) :
s.w_opp_side x z
theorem
affine_subspace.s_same_side.trans_s_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.s_same_side x y)
(hyz : s.s_opp_side y z) :
s.s_opp_side x z
theorem
affine_subspace.w_opp_side.trans_w_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.w_opp_side x y)
(hyz : s.w_same_side y z)
(hy : y ∉ s) :
s.w_opp_side x z
theorem
affine_subspace.w_opp_side.trans_s_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.w_opp_side x y)
(hyz : s.s_same_side y z) :
s.w_opp_side x z
theorem
affine_subspace.w_opp_side.trans
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.w_opp_side x y)
(hyz : s.w_opp_side y z)
(hy : y ∉ s) :
s.w_same_side x z
theorem
affine_subspace.w_opp_side.trans_s_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.w_opp_side x y)
(hyz : s.s_opp_side y z) :
s.w_same_side x z
theorem
affine_subspace.s_opp_side.trans_w_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.s_opp_side x y)
(hyz : s.w_same_side y z) :
s.w_opp_side x z
theorem
affine_subspace.s_opp_side.trans_s_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.s_opp_side x y)
(hyz : s.s_same_side y z) :
s.s_opp_side x z
theorem
affine_subspace.s_opp_side.trans_w_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.s_opp_side x y)
(hyz : s.w_opp_side y z) :
s.w_same_side x z
theorem
affine_subspace.s_opp_side.trans
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(hxy : s.s_opp_side x y)
(hyz : s.s_opp_side y z) :
s.s_same_side x z
theorem
affine_subspace.w_same_side_and_w_opp_side_iff
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
s.w_same_side x y ∧ s.w_opp_side x y ↔ x ∈ s ∨ y ∈ s
theorem
affine_subspace.w_same_side.not_s_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.w_same_side x y) :
¬s.s_opp_side x y
theorem
affine_subspace.s_same_side.not_w_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_same_side x y) :
¬s.w_opp_side x y
theorem
affine_subspace.s_same_side.not_s_opp_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_same_side x y) :
¬s.s_opp_side x y
theorem
affine_subspace.w_opp_side.not_s_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.w_opp_side x y) :
¬s.s_same_side x y
theorem
affine_subspace.s_opp_side.not_w_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_opp_side x y) :
¬s.w_same_side x y
theorem
affine_subspace.s_opp_side.not_s_same_side
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_opp_side x y) :
¬s.s_same_side x y
theorem
affine_subspace.w_opp_side_iff_exists_wbtw
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P} :
theorem
affine_subspace.s_opp_side.exists_sbtw
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(h : s.s_opp_side x y) :
theorem
sbtw.s_opp_side_of_not_mem_of_mem
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y z : P}
(h : sbtw R x y z)
(hx : x ∉ s)
(hy : y ∈ s) :
s.s_opp_side x z
theorem
affine_subspace.s_same_side_smul_vsub_vadd_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x p₁ p₂ : P}
(hx : x ∉ s)
(hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s)
{t : R}
(ht : 0 < t) :
s.s_same_side (t • (x -ᵥ p₁) +ᵥ p₂) x
theorem
affine_subspace.s_same_side_smul_vsub_vadd_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x p₁ p₂ : P}
(hx : x ∉ s)
(hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s)
{t : R}
(ht : 0 < t) :
s.s_same_side x (t • (x -ᵥ p₁) +ᵥ p₂)
theorem
affine_subspace.s_same_side_line_map_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(hx : x ∈ s)
(hy : y ∉ s)
{t : R}
(ht : 0 < t) :
s.s_same_side (⇑(affine_map.line_map x y) t) y
theorem
affine_subspace.s_same_side_line_map_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(hx : x ∈ s)
(hy : y ∉ s)
{t : R}
(ht : 0 < t) :
s.s_same_side y (⇑(affine_map.line_map x y) t)
theorem
affine_subspace.s_opp_side_smul_vsub_vadd_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x p₁ p₂ : P}
(hx : x ∉ s)
(hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s)
{t : R}
(ht : t < 0) :
s.s_opp_side (t • (x -ᵥ p₁) +ᵥ p₂) x
theorem
affine_subspace.s_opp_side_smul_vsub_vadd_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x p₁ p₂ : P}
(hx : x ∉ s)
(hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s)
{t : R}
(ht : t < 0) :
s.s_opp_side x (t • (x -ᵥ p₁) +ᵥ p₂)
theorem
affine_subspace.s_opp_side_line_map_left
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(hx : x ∈ s)
(hy : y ∉ s)
{t : R}
(ht : t < 0) :
s.s_opp_side (⇑(affine_map.line_map x y) t) y
theorem
affine_subspace.s_opp_side_line_map_right
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(hx : x ∈ s)
(hy : y ∉ s)
{t : R}
(ht : t < 0) :
s.s_opp_side y (⇑(affine_map.line_map x y) t)
theorem
affine_subspace.set_of_w_same_side_eq_image2
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x p : P}
(hx : x ∉ s)
(hp : p ∈ s) :
{y : P | s.w_same_side x y} = set.image2 (λ (t : R) (q : P), t • (x -ᵥ p) +ᵥ q) (set.Ici 0) ↑s
theorem
affine_subspace.set_of_s_same_side_eq_image2
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x p : P}
(hx : x ∉ s)
(hp : p ∈ s) :
{y : P | s.s_same_side x y} = set.image2 (λ (t : R) (q : P), t • (x -ᵥ p) +ᵥ q) (set.Ioi 0) ↑s
theorem
affine_subspace.set_of_w_opp_side_eq_image2
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x p : P}
(hx : x ∉ s)
(hp : p ∈ s) :
{y : P | s.w_opp_side x y} = set.image2 (λ (t : R) (q : P), t • (x -ᵥ p) +ᵥ q) (set.Iic 0) ↑s
theorem
affine_subspace.set_of_s_opp_side_eq_image2
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x p : P}
(hx : x ∉ s)
(hp : p ∈ s) :
{y : P | s.s_opp_side x y} = set.image2 (λ (t : R) (q : P), t • (x -ᵥ p) +ᵥ q) (set.Iio 0) ↑s
theorem
affine_subspace.w_opp_side_point_reflection
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x : P}
(y : P)
(hx : x ∈ s) :
s.w_opp_side y (⇑(affine_equiv.point_reflection R x) y)
theorem
affine_subspace.s_opp_side_point_reflection
{R : Type u_1}
{V : Type u_2}
{P : Type u_4}
[linear_ordered_field R]
[add_comm_group V]
[module R V]
[add_torsor V P]
{s : affine_subspace R P}
{x y : P}
(hx : x ∈ s)
(hy : y ∉ s) :
s.s_opp_side y (⇑(affine_equiv.point_reflection R x) y)
theorem
affine_subspace.is_connected_set_of_w_same_side
{V : Type u_2}
{P : Type u_4}
[seminormed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{s : affine_subspace ℝ P}
(x : P)
(h : ↑s.nonempty) :
is_connected {y : P | s.w_same_side x y}
theorem
affine_subspace.is_preconnected_set_of_w_same_side
{V : Type u_2}
{P : Type u_4}
[seminormed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(s : affine_subspace ℝ P)
(x : P) :
is_preconnected {y : P | s.w_same_side x y}
theorem
affine_subspace.is_connected_set_of_s_same_side
{V : Type u_2}
{P : Type u_4}
[seminormed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{s : affine_subspace ℝ P}
{x : P}
(hx : x ∉ s)
(h : ↑s.nonempty) :
is_connected {y : P | s.s_same_side x y}
theorem
affine_subspace.is_preconnected_set_of_s_same_side
{V : Type u_2}
{P : Type u_4}
[seminormed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(s : affine_subspace ℝ P)
(x : P) :
is_preconnected {y : P | s.s_same_side x y}
theorem
affine_subspace.is_connected_set_of_w_opp_side
{V : Type u_2}
{P : Type u_4}
[seminormed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{s : affine_subspace ℝ P}
(x : P)
(h : ↑s.nonempty) :
is_connected {y : P | s.w_opp_side x y}
theorem
affine_subspace.is_preconnected_set_of_w_opp_side
{V : Type u_2}
{P : Type u_4}
[seminormed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(s : affine_subspace ℝ P)
(x : P) :
is_preconnected {y : P | s.w_opp_side x y}
theorem
affine_subspace.is_connected_set_of_s_opp_side
{V : Type u_2}
{P : Type u_4}
[seminormed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{s : affine_subspace ℝ P}
{x : P}
(hx : x ∉ s)
(h : ↑s.nonempty) :
is_connected {y : P | s.s_opp_side x y}
theorem
affine_subspace.is_preconnected_set_of_s_opp_side
{V : Type u_2}
{P : Type u_4}
[seminormed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(s : affine_subspace ℝ P)
(x : P) :
is_preconnected {y : P | s.s_opp_side x y}