Sides of affine subspaces

This file defines notions of two points being on the same or opposite sides of an affine subspace.

Main definitions

• s.WSameSide x y: The points x and y are weakly on the same side of the affine subspace s.
• s.SSameSide x y: The points x and y are strictly on the same side of the affine subspace s.
• s.WOppSide x y: The points x and y are weakly on opposite sides of the affine subspace s.
• s.SOppSide x y: The points x and y are strictly on opposite sides of the affine subspace s.

def AffineSubspace.WSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x y : P) : Prop

The points x and y are weakly on the same side of s.

Equations

• s.WSameSide x y = ∃ p₁ ∈ s, ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

def AffineSubspace.SSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x y : P) : Prop

The points x and y are strictly on the same side of s.

Equations

• s.SSameSide x y = (s.WSameSide x y ∧ x ∉ s ∧ y ∉ s)

def AffineSubspace.WOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x y : P) : Prop

The points x and y are weakly on opposite sides of s.

Equations

• s.WOppSide x y = ∃ p₁ ∈ s, ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

def AffineSubspace.SOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x y : P) : Prop

The points x and y are strictly on opposite sides of s.

Equations

• s.SOppSide x y = (s.WOppSide x y ∧ x ∉ s ∧ y ∉ s)

theorem AffineSubspace.WSameSide.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} (h : s.WSameSide x y) (f : P →ᵃ[R] P') : (AffineSubspace.map f s).WSameSide (f x) (f y)

theorem Function.Injective.wSameSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'} (hf : Injective ⇑f) : (AffineSubspace.map f s).WSameSide (f x) (f y) ↔ s.WSameSide x y

theorem Function.Injective.sSameSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'} (hf : Injective ⇑f) : (AffineSubspace.map f s).SSameSide (f x) (f y) ↔ s.SSameSide x y

@[simp]

theorem AffineEquiv.wSameSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} (f : P ≃ᵃ[R] P') : (AffineSubspace.map (↑f) s).WSameSide (f x) (f y) ↔ s.WSameSide x y

@[simp]

theorem AffineEquiv.sSameSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} (f : P ≃ᵃ[R] P') : (AffineSubspace.map (↑f) s).SSameSide (f x) (f y) ↔ s.SSameSide x y

theorem AffineSubspace.WOppSide.map {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} (h : s.WOppSide x y) (f : P →ᵃ[R] P') : (AffineSubspace.map f s).WOppSide (f x) (f y)

theorem Function.Injective.wOppSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'} (hf : Injective ⇑f) : (AffineSubspace.map f s).WOppSide (f x) (f y) ↔ s.WOppSide x y

theorem Function.Injective.sOppSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'} (hf : Injective ⇑f) : (AffineSubspace.map f s).SOppSide (f x) (f y) ↔ s.SOppSide x y

@[simp]

theorem AffineEquiv.wOppSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} (f : P ≃ᵃ[R] P') : (AffineSubspace.map (↑f) s).WOppSide (f x) (f y) ↔ s.WOppSide x y

@[simp]

theorem AffineEquiv.sOppSide_map_iff {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] {s : AffineSubspace R P} {x y : P} (f : P ≃ᵃ[R] P') : (AffineSubspace.map (↑f) s).SOppSide (f x) (f y) ↔ s.SOppSide x y

theorem AffineSubspace.WSameSide.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.WSameSide x y) : (↑s).Nonempty

theorem AffineSubspace.SSameSide.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SSameSide x y) : (↑s).Nonempty

theorem AffineSubspace.WOppSide.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.WOppSide x y) : (↑s).Nonempty

theorem AffineSubspace.SOppSide.nonempty {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : (↑s).Nonempty

theorem AffineSubspace.SSameSide.wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SSameSide x y) : s.WSameSide x y

theorem AffineSubspace.SSameSide.left_notMem {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SSameSide x y) : x ∉ s

theorem AffineSubspace.SSameSide.right_notMem {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SSameSide x y) : y ∉ s

theorem AffineSubspace.SOppSide.wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : s.WOppSide x y

theorem AffineSubspace.SOppSide.left_notMem {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : x ∉ s

theorem AffineSubspace.SOppSide.right_notMem {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : y ∉ s

theorem AffineSubspace.wSameSide_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.WSameSide x y ↔ s.WSameSide y x

theorem AffineSubspace.WSameSide.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.WSameSide x y → s.WSameSide y x

Alias of the forward direction of AffineSubspace.wSameSide_comm.

theorem AffineSubspace.sSameSide_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.SSameSide x y ↔ s.SSameSide y x

theorem AffineSubspace.SSameSide.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.SSameSide x y → s.SSameSide y x

Alias of the forward direction of AffineSubspace.sSameSide_comm.

theorem AffineSubspace.wOppSide_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.WOppSide x y ↔ s.WOppSide y x

theorem AffineSubspace.WOppSide.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.WOppSide x y → s.WOppSide y x

Alias of the forward direction of AffineSubspace.wOppSide_comm.

theorem AffineSubspace.sOppSide_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.SOppSide x y ↔ s.SOppSide y x

theorem AffineSubspace.SOppSide.symm {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.SOppSide x y → s.SOppSide y x

Alias of the forward direction of AffineSubspace.sOppSide_comm.

theorem AffineSubspace.not_wSameSide_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : ¬⊥.WSameSide x y

theorem AffineSubspace.not_sSameSide_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : ¬⊥.SSameSide x y

theorem AffineSubspace.not_wOppSide_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : ¬⊥.WOppSide x y

theorem AffineSubspace.not_sOppSide_bot {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (x y : P) : ¬⊥.SOppSide x y

@[simp]

theorem AffineSubspace.wSameSide_self_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} : s.WSameSide x x ↔ (↑s).Nonempty

theorem AffineSubspace.sSameSide_self_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} : s.SSameSide x x ↔ (↑s).Nonempty ∧ x ∉ s

theorem AffineSubspace.wSameSide_of_left_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (hx : x ∈ s) : s.WSameSide x y

theorem AffineSubspace.wSameSide_of_right_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} (x : P) {y : P} (hy : y ∈ s) : s.WSameSide x y

theorem AffineSubspace.wOppSide_of_left_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (hx : x ∈ s) : s.WOppSide x y

theorem AffineSubspace.wOppSide_of_right_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} (x : P) {y : P} (hy : y ∈ s) : s.WOppSide x y

theorem AffineSubspace.wSameSide_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) : s.WSameSide (v +ᵥ x) y ↔ s.WSameSide x y

theorem AffineSubspace.wSameSide_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) : s.WSameSide x (v +ᵥ y) ↔ s.WSameSide x y

theorem AffineSubspace.sSameSide_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) : s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y

theorem AffineSubspace.sSameSide_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) : s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y

theorem AffineSubspace.wOppSide_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) : s.WOppSide (v +ᵥ x) y ↔ s.WOppSide x y

theorem AffineSubspace.wOppSide_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) : s.WOppSide x (v +ᵥ y) ↔ s.WOppSide x y

theorem AffineSubspace.sOppSide_vadd_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) : s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y

theorem AffineSubspace.sOppSide_vadd_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) : s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y

theorem AffineSubspace.wSameSide_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : 0 ≤ t) : s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

theorem AffineSubspace.wSameSide_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : 0 ≤ t) : s.WSameSide x (t • (x -ᵥ p₁) +ᵥ p₂)

theorem AffineSubspace.wSameSide_lineMap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (h : x ∈ s) {t : R} (ht : 0 ≤ t) : s.WSameSide ((AffineMap.lineMap x y) t) y

theorem AffineSubspace.wSameSide_lineMap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (h : x ∈ s) {t : R} (ht : 0 ≤ t) : s.WSameSide y ((AffineMap.lineMap x y) t)

theorem AffineSubspace.wOppSide_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : t ≤ 0) : s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

theorem AffineSubspace.wOppSide_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : t ≤ 0) : s.WOppSide x (t • (x -ᵥ p₁) +ᵥ p₂)

theorem AffineSubspace.wOppSide_lineMap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (h : x ∈ s) {t : R} (ht : t ≤ 0) : s.WOppSide ((AffineMap.lineMap x y) t) y

theorem AffineSubspace.wOppSide_lineMap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (h : x ∈ s) {t : R} (ht : t ≤ 0) : s.WOppSide y ((AffineMap.lineMap x y) t)

theorem Wbtw.wSameSide₂₃ {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hx : x ∈ s) : s.WSameSide y z

theorem Wbtw.wSameSide₃₂ {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hx : x ∈ s) : s.WSameSide z y

theorem Wbtw.wSameSide₁₂ {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hz : z ∈ s) : s.WSameSide x y

theorem Wbtw.wSameSide₂₁ {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hz : z ∈ s) : s.WSameSide y x

theorem Wbtw.wOppSide₁₃ {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hy : y ∈ s) : s.WOppSide x z

theorem Wbtw.wOppSide₃₁ {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hy : y ∈ s) : s.WOppSide z x

theorem AffineSubspace.wSameSide_of_vsub_eq_smul {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₁ p₂ : P} {m : V} {c₁ c₂ : R} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h₁ : x -ᵥ p₁ = c₁ • m) (h₂ : y -ᵥ p₂ = c₂ • m) (hc : 0 ≤ c₁ * c₂) : s.WSameSide x y

If x and y are displaced from points of s by multiples of a common vector whose coefficients have nonnegative product, they are weakly on the same side of s.

theorem AffineSubspace.wOppSide_of_vsub_eq_smul {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₁ p₂ : P} {m : V} {c₁ c₂ : R} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h₁ : x -ᵥ p₁ = c₁ • m) (h₂ : y -ᵥ p₂ = c₂ • m) (hc : c₁ * c₂ ≤ 0) : s.WOppSide x y

If x and y are displaced from points of s by multiples of a common vector whose coefficients have nonpositive product, they are weakly on opposite sides of s.

theorem AffineSubspace.sSameSide_of_vsub_eq_smul {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₁ p₂ : P} {m : V} {c₁ c₂ : R} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h₁ : x -ᵥ p₁ = c₁ • m) (h₂ : y -ᵥ p₂ = c₂ • m) (hc : 0 ≤ c₁ * c₂) (hx : x ∉ s) (hy : y ∉ s) : s.SSameSide x y

If x and y lie off s and are displaced from points of s by multiples of a common vector whose coefficients have nonnegative product, they are strictly on the same side of s.

theorem AffineSubspace.sOppSide_of_vsub_eq_smul {R : Type u_1} {V : Type u_2} {P : Type u_4} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₁ p₂ : P} {m : V} {c₁ c₂ : R} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (h₁ : x -ᵥ p₁ = c₁ • m) (h₂ : y -ᵥ p₂ = c₂ • m) (hc : c₁ * c₂ ≤ 0) (hx : x ∉ s) (hy : y ∉ s) : s.SOppSide x y

If x and y lie off s and are displaced from points of s by multiples of a common vector whose coefficients have nonpositive product, they are strictly on opposite sides of s.

@[simp]

theorem AffineSubspace.wOppSide_self_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} : s.WOppSide x x ↔ x ∈ s

theorem AffineSubspace.not_sOppSide_self {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : AffineSubspace R P) (x : P) : ¬s.SOppSide x x

theorem AffineSubspace.wSameSide_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) : s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

theorem AffineSubspace.wSameSide_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) : s.WSameSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

theorem AffineSubspace.sSameSide_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) : s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

theorem AffineSubspace.sSameSide_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) : s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

theorem AffineSubspace.wOppSide_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) : s.WOppSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

theorem AffineSubspace.wOppSide_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) : s.WOppSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

theorem AffineSubspace.sOppSide_iff_exists_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) : s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

theorem AffineSubspace.sOppSide_iff_exists_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) : s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

theorem AffineSubspace.WSameSide.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.WSameSide x y) (hyz : s.WSameSide y z) (hy : y ∉ s) : s.WSameSide x z

theorem AffineSubspace.WSameSide.trans_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.WSameSide x y) (hyz : s.SSameSide y z) : s.WSameSide x z

theorem AffineSubspace.WSameSide.trans_wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.WSameSide x y) (hyz : s.WOppSide y z) (hy : y ∉ s) : s.WOppSide x z

theorem AffineSubspace.WSameSide.trans_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.WSameSide x y) (hyz : s.SOppSide y z) : s.WOppSide x z

theorem AffineSubspace.SSameSide.trans_wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.SSameSide x y) (hyz : s.WSameSide y z) : s.WSameSide x z

theorem AffineSubspace.SSameSide.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.SSameSide x y) (hyz : s.SSameSide y z) : s.SSameSide x z

theorem AffineSubspace.SSameSide.trans_wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.SSameSide x y) (hyz : s.WOppSide y z) : s.WOppSide x z

theorem AffineSubspace.SSameSide.trans_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.SSameSide x y) (hyz : s.SOppSide y z) : s.SOppSide x z

theorem AffineSubspace.WOppSide.trans_wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.WOppSide x y) (hyz : s.WSameSide y z) (hy : y ∉ s) : s.WOppSide x z

theorem AffineSubspace.WOppSide.trans_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.WOppSide x y) (hyz : s.SSameSide y z) : s.WOppSide x z

theorem AffineSubspace.WOppSide.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.WOppSide x y) (hyz : s.WOppSide y z) (hy : y ∉ s) : s.WSameSide x z

theorem AffineSubspace.WOppSide.trans_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.WOppSide x y) (hyz : s.SOppSide y z) : s.WSameSide x z

theorem AffineSubspace.SOppSide.trans_wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.SOppSide x y) (hyz : s.WSameSide y z) : s.WOppSide x z

theorem AffineSubspace.SOppSide.trans_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.SOppSide x y) (hyz : s.SSameSide y z) : s.SOppSide x z

theorem AffineSubspace.SOppSide.trans_wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.SOppSide x y) (hyz : s.WOppSide y z) : s.WSameSide x z

theorem AffineSubspace.SOppSide.trans {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (hxy : s.SOppSide x y) (hyz : s.SOppSide y z) : s.SSameSide x z

theorem AffineSubspace.wSameSide_and_wOppSide_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.WSameSide x y ∧ s.WOppSide x y ↔ x ∈ s ∨ y ∈ s

theorem AffineSubspace.WSameSide.not_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.WSameSide x y) : ¬s.SOppSide x y

theorem AffineSubspace.SSameSide.not_wOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SSameSide x y) : ¬s.WOppSide x y

theorem AffineSubspace.SSameSide.not_sOppSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SSameSide x y) : ¬s.SOppSide x y

theorem AffineSubspace.WOppSide.not_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.WOppSide x y) : ¬s.SSameSide x y

theorem AffineSubspace.SOppSide.not_wSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : ¬s.WSameSide x y

theorem AffineSubspace.SOppSide.not_sSameSide {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : ¬s.SSameSide x y

theorem AffineSubspace.wOppSide_iff_exists_wbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} : s.WOppSide x y ↔ ∃ p ∈ s, Wbtw R x p y

theorem AffineSubspace.SOppSide.exists_sbtw {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : ∃ p ∈ s, Sbtw R x p y

theorem Sbtw.sOppSide_of_notMem_of_mem {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y z : P} (h : Sbtw R x y z) (hx : x ∉ s) (hy : y ∈ s) : s.SOppSide x z

theorem AffineSubspace.sSameSide_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p₁ p₂ : P} (hx : x ∉ s) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : 0 < t) : s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

theorem AffineSubspace.sSameSide_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p₁ p₂ : P} (hx : x ∉ s) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : 0 < t) : s.SSameSide x (t • (x -ᵥ p₁) +ᵥ p₂)

theorem AffineSubspace.sSameSide_lineMap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (hx : x ∈ s) (hy : y ∉ s) {t : R} (ht : 0 < t) : s.SSameSide ((AffineMap.lineMap x y) t) y

theorem AffineSubspace.sSameSide_lineMap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (hx : x ∈ s) (hy : y ∉ s) {t : R} (ht : 0 < t) : s.SSameSide y ((AffineMap.lineMap x y) t)

theorem AffineSubspace.sOppSide_smul_vsub_vadd_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p₁ p₂ : P} (hx : x ∉ s) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : t < 0) : s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x

theorem AffineSubspace.sOppSide_smul_vsub_vadd_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p₁ p₂ : P} (hx : x ∉ s) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : t < 0) : s.SOppSide x (t • (x -ᵥ p₁) +ᵥ p₂)

theorem AffineSubspace.sOppSide_lineMap_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (hx : x ∈ s) (hy : y ∉ s) {t : R} (ht : t < 0) : s.SOppSide ((AffineMap.lineMap x y) t) y

theorem AffineSubspace.sOppSide_lineMap_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (hx : x ∈ s) (hy : y ∉ s) {t : R} (ht : t < 0) : s.SOppSide y ((AffineMap.lineMap x y) t)

theorem AffineSubspace.setOfPred_wSameSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : {y : P | s.WSameSide x y} = Set.image2 (fun (t : R) (q : P) => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s

@[deprecated AffineSubspace.setOfPred_wSameSide_eq_image2 (since := "2026-07-09")]

theorem AffineSubspace.setOf_wSameSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : {y : P | s.WSameSide x y} = Set.image2 (fun (t : R) (q : P) => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s

Alias of AffineSubspace.setOfPred_wSameSide_eq_image2.

theorem AffineSubspace.setOfPred_sSameSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : {y : P | s.SSameSide x y} = Set.image2 (fun (t : R) (q : P) => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s

@[deprecated AffineSubspace.setOfPred_sSameSide_eq_image2 (since := "2026-07-09")]

theorem AffineSubspace.setOf_sSameSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : {y : P | s.SSameSide x y} = Set.image2 (fun (t : R) (q : P) => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s

Alias of AffineSubspace.setOfPred_sSameSide_eq_image2.

theorem AffineSubspace.setOfPred_wOppSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : {y : P | s.WOppSide x y} = Set.image2 (fun (t : R) (q : P) => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s

@[deprecated AffineSubspace.setOfPred_wOppSide_eq_image2 (since := "2026-07-09")]

theorem AffineSubspace.setOf_wOppSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : {y : P | s.WOppSide x y} = Set.image2 (fun (t : R) (q : P) => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) ↑s

Alias of AffineSubspace.setOfPred_wOppSide_eq_image2.

theorem AffineSubspace.setOfPred_sOppSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : {y : P | s.SOppSide x y} = Set.image2 (fun (t : R) (q : P) => t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s

@[deprecated AffineSubspace.setOfPred_sOppSide_eq_image2 (since := "2026-07-09")]

theorem AffineSubspace.setOf_sOppSide_eq_image2 {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : {y : P | s.SOppSide x y} = Set.image2 (fun (t : R) (q : P) => t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s

Alias of AffineSubspace.setOfPred_sOppSide_eq_image2.

theorem AffineSubspace.wOppSide_pointReflection {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x : P} (y : P) (hx : x ∈ s) : s.WOppSide y ((AffineEquiv.pointReflection R x) y)

theorem AffineSubspace.sOppSide_pointReflection {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {s : AffineSubspace R P} {x y : P} (hx : x ∈ s) (hy : y ∉ s) : s.SOppSide y ((AffineEquiv.pointReflection R x) y)

theorem AffineSubspace.isConnected_setOfPred_wSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} (x : P) (h : (↑s).Nonempty) : IsConnected {y : P | s.WSameSide x y}

@[deprecated AffineSubspace.isConnected_setOfPred_wSameSide (since := "2026-07-09")]

theorem AffineSubspace.isConnected_setOf_wSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} (x : P) (h : (↑s).Nonempty) : IsConnected {y : P | s.WSameSide x y}

Alias of AffineSubspace.isConnected_setOfPred_wSameSide.

theorem AffineSubspace.isPreconnected_setOfPred_wSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y : P | s.WSameSide x y}

@[deprecated AffineSubspace.isPreconnected_setOfPred_wSameSide (since := "2026-07-09")]

theorem AffineSubspace.isPreconnected_setOf_wSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y : P | s.WSameSide x y}

Alias of AffineSubspace.isPreconnected_setOfPred_wSameSide.

theorem AffineSubspace.isConnected_setOfPred_sSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {x : P} (hx : x ∉ s) (h : (↑s).Nonempty) : IsConnected {y : P | s.SSameSide x y}

@[deprecated AffineSubspace.isConnected_setOfPred_sSameSide (since := "2026-07-09")]

theorem AffineSubspace.isConnected_setOf_sSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {x : P} (hx : x ∉ s) (h : (↑s).Nonempty) : IsConnected {y : P | s.SSameSide x y}

Alias of AffineSubspace.isConnected_setOfPred_sSameSide.

theorem AffineSubspace.isPreconnected_setOfPred_sSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y : P | s.SSameSide x y}

@[deprecated AffineSubspace.isPreconnected_setOfPred_sSameSide (since := "2026-07-09")]

theorem AffineSubspace.isPreconnected_setOf_sSameSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y : P | s.SSameSide x y}

Alias of AffineSubspace.isPreconnected_setOfPred_sSameSide.

theorem AffineSubspace.isConnected_setOfPred_wOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} (x : P) (h : (↑s).Nonempty) : IsConnected {y : P | s.WOppSide x y}

@[deprecated AffineSubspace.isConnected_setOfPred_wOppSide (since := "2026-07-09")]

theorem AffineSubspace.isConnected_setOf_wOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} (x : P) (h : (↑s).Nonempty) : IsConnected {y : P | s.WOppSide x y}

Alias of AffineSubspace.isConnected_setOfPred_wOppSide.

theorem AffineSubspace.isPreconnected_setOfPred_wOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y : P | s.WOppSide x y}

@[deprecated AffineSubspace.isPreconnected_setOfPred_wOppSide (since := "2026-07-09")]

theorem AffineSubspace.isPreconnected_setOf_wOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y : P | s.WOppSide x y}

Alias of AffineSubspace.isPreconnected_setOfPred_wOppSide.

theorem AffineSubspace.isConnected_setOfPred_sOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {x : P} (hx : x ∉ s) (h : (↑s).Nonempty) : IsConnected {y : P | s.SOppSide x y}

@[deprecated AffineSubspace.isConnected_setOfPred_sOppSide (since := "2026-07-09")]

theorem AffineSubspace.isConnected_setOf_sOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} {x : P} (hx : x ∉ s) (h : (↑s).Nonempty) : IsConnected {y : P | s.SOppSide x y}

Alias of AffineSubspace.isConnected_setOfPred_sOppSide.

theorem AffineSubspace.isPreconnected_setOfPred_sOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y : P | s.SOppSide x y}

@[deprecated AffineSubspace.isPreconnected_setOfPred_sOppSide (since := "2026-07-09")]

theorem AffineSubspace.isPreconnected_setOf_sOppSide {V : Type u_2} {P : Type u_4} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y : P | s.SOppSide x y}

Alias of AffineSubspace.isPreconnected_setOfPred_sOppSide.

theorem Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j : Fin (n + 1), w₁ j = 1) (hw₂ : ∑ j : Fin (n + 1), w₂ j = 1) {i : Fin (n + 1)} (hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)) (h0 : w₁ i ≠ 0) : (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂)

theorem Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_neg {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j : Fin (n + 1), w₁ j = 1) (hw₂ : ∑ j : Fin (n + 1), w₂ j = 1) {i : Fin (n + 1)} (hs₁ : 0 < w₁ i) (hs₂ : w₂ i < 0) : (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂)

theorem Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j : Fin (n + 1), w₁ j = 1) (hw₂ : ∑ j : Fin (n + 1), w₂ j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂) ↔ SignType.sign (w₁ i) = SignType.sign (w₂ i) ∧ w₁ i ≠ 0

theorem Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j : Fin (n + 1), w₁ j = 1) (hw₂ : ∑ j : Fin (n + 1), w₂ j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂) ↔ SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∧ w₁ i ≠ 0

theorem Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j : Fin (n + 1), w₁ j = 1) (hw₂ : ∑ j : Fin (n + 1), w₂ j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂) ↔ SignType.sign (w₁ i) = SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0

theorem Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w₁ w₂ : Fin (n + 1) → R} (hw₁ : ∑ j : Fin (n + 1), w₁ j = 1) (hw₂ : ∑ j : Fin (n + 1), w₂ j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₂) ↔ SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0

theorem Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w : Fin (n + 1) → R} (hw : ∑ j : Fin (n + 1), w j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide (s.points i) ((Finset.affineCombination R Finset.univ s.points) w) ↔ 0 < w i

theorem Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w : Fin (n + 1) → R} (hw : ∑ j : Fin (n + 1), w j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w) (s.points i) ↔ 0 < w i

theorem Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w : Fin (n + 1) → R} (hw : ∑ j : Fin (n + 1), w j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide (s.points i) ((Finset.affineCombination R Finset.univ s.points) w) ↔ w i < 0

theorem Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w : Fin (n + 1) → R} (hw : ∑ j : Fin (n + 1), w j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w) (s.points i) ↔ w i < 0

theorem Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w : Fin (n + 1) → R} (hw : ∑ j : Fin (n + 1), w j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide (s.points i) ((Finset.affineCombination R Finset.univ s.points) w) ↔ 0 ≤ w i

theorem Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w : Fin (n + 1) → R} (hw : ∑ j : Fin (n + 1), w j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide ((Finset.affineCombination R Finset.univ s.points) w) (s.points i) ↔ 0 ≤ w i

theorem Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w : Fin (n + 1) → R} (hw : ∑ j : Fin (n + 1), w j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide (s.points i) ((Finset.affineCombination R Finset.univ s.points) w) ↔ w i ≤ 0

theorem Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_right_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex R P n) {w : Fin (n + 1) → R} (hw : ∑ j : Fin (n + 1), w j = 1) {i : Fin (n + 1)} : (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide ((Finset.affineCombination R Finset.univ s.points) w) (s.points i) ↔ w i ≤ 0