AffineSubspace.WSameSide.trans_wOppSide
theorem AffineSubspace.WSameSide.trans_wOppSide :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : LinearOrderedField R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {x y z : P},
s.WSameSide x y → s.WOppSide y z → y ∉ s → s.WOppSide x z
The theorem `AffineSubspace.WSameSide.trans_wOppSide` states that given an affine subspace `s` and three points `x`, `y`, and `z`, if `x` and `y` are weakly on the same side of `s` and `y` and `z` are weakly on opposite sides of `s`, and if `y` does not belong to `s`, then `x` and `z` are weakly on opposite sides of `s`.
In more detail, the "weakly on the same side" relation means that there exist two points in the subspace such that the vectors from each of these points to `x` and `y` are on the same ray (line passing through the origin). The "weakly on opposite sides" relation means that there exist two points in the subspace such that the vectors from each of these points to `y` and `z` are on the same ray, but pointed in opposite directions.
More concisely: Given an affine subspace and three points x, y, z such that x and y are weakly on the same side and y and z are weakly on opposite sides with y not belonging to the subspace, then x and z are weakly on opposite sides of the subspace.
|
AffineSubspace.SSameSide.symm
theorem AffineSubspace.SSameSide.symm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : StrictOrderedCommRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {x y : P},
s.SSameSide x y → s.SSameSide y x
The theorem `AffineSubspace.SSameSide.symm` states that for any affine subspace `s` and points `x` and `y`, if `x` and `y` are strictly on the same side of `s`, then `y` and `x` are also strictly on the same side of `s`. This is conducted under the conditions that `R` is a strictly ordered commutative ring, `V` is an additive commutative group, `P` is an affine space over `V` with `R` as scalars, and both `x` and `y` are not in `s`. The theorem thus asserts the symmetry of the relation "being strictly on the same side of a subspace".
More concisely: If `x` and `y` are strictly on the same side of an affine subspace `s` in an affine space `P` over a strictly ordered commutative ring `R`, then `y` and `x` are also strictly on the same side of `s`.
|
AffineSubspace.SOppSide.symm
theorem AffineSubspace.SOppSide.symm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : StrictOrderedCommRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {x y : P},
s.SOppSide x y → s.SOppSide y x
This theorem, named `AffineSubspace.SOppSide.symm`, asserts that for a given strict ordered commutative ring `R`, an additive commutative group `V`, a module `R` over `V`, a torsor `P` for `V`, an affine subspace `s` of `R` in `P`, and points `x` and `y` in `P`, if `x` and `y` are strictly on opposite sides of `s` (i.e., `AffineSubspace.SOppSide s x y` holds), then `y` and `x` are also strictly on opposite sides of `s` (i.e., `AffineSubspace.SOppSide s y x` holds). This theorem is actually the symmetric version of the property `AffineSubspace.sOppSide_comm`.
More concisely: For an affine subspace `s` of a module `P` over a commutative ring `R`, and points `x` and `y` in `P` strictly on opposite sides of `s`, we have that `x` and `y` are also strictly on opposite sides of `s`, i.e., `AffineSubspace.SOppSide s x y` implies `AffineSubspace.SOppSide s y x`.
|
AffineSubspace.SSameSide.wSameSide
theorem AffineSubspace.SSameSide.wSameSide :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : StrictOrderedCommRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {x y : P},
s.SSameSide x y → s.WSameSide x y
This theorem states that for any strict ordered commutative ring `R`, additive commutative group `V`, module `V` over `R`, additive torsor `P` over `V`, affine subspace `s` of `P`, and points `x` and `y` in `P`, if `x` and `y` are strictly on the same side of `s` (which means they are on the same side of `s` and both are not in `s`), then `x` and `y` are weakly on the same side of `s`.
In the weak sense, `x` and `y` being on the same side of `s` means that there exist points `p₁` and `p₂` in `s` such that `x - p₁` and `y - p₂` are in the same ray in `R` (they are scalar multiples of each other where the scalar is non-negative).
More concisely: For any strict ordered commutative ring `R`, additive commutative group `V` with `R`-module structure, additive torsor `P` over `V`, affine subspace `s` of `P`, and points `x, y` in `P` not lying in `s`, if `x` and `y` are strictly on the same side of `s`, then `x - y` and `y - x` generate the same ray in `R^+`, the set of non-negative elements of `R`.
|
AffineSubspace.WOppSide.symm
theorem AffineSubspace.WOppSide.symm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : StrictOrderedCommRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {x y : P},
s.WOppSide x y → s.WOppSide y x
The theorem `AffineSubspace.WOppSide.symm` states that for any strict ordered commutative ring `R`, additive commutative group `V`, module `R V`, and additive torsor `V P`, given an affine subspace `s` of `R P` and points `x` and `y` of `P`, if `x` and `y` are weakly on opposite sides of `s`, then `y` and `x` are also weakly on opposite sides of `s`.
Here, points `x` and `y` being weakly on opposite sides of `s` means that there exists pair of points `p₁` and `p₂` in `s` such that the vector pointing from `x` to `p₁` and the vector pointing from `p₂` to `y` are on the same ray. The theorem ensures this condition is symmetric.
More concisely: If points `x` and `y` in a set `P` are weakly opposite sides of an affine subspace `s` in a module `R V` over a commutative ring `R`, then `y` and `x` are also weakly opposite sides of `s`.
|
AffineSubspace.wSameSide_smul_vsub_vadd_left
theorem AffineSubspace.wSameSide_smul_vsub_vadd_left :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : StrictOrderedCommRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {p₁ p₂ : P} (x : P),
p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, 0 ≤ t → s.WSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x
The theorem `AffineSubspace.wSameSide_smul_vsub_vadd_left` states that for any strict ordered commutative ring `R`, an additive commutative group `V`, a module `V` over `R`, an "additive torsor" `P` over `V`, an affine subspace `s` of `P`, and points `p₁`, `p₂`, and `x` in `P`, if `p₁` and `p₂` belong to the subspace `s` and a scalar `t` from `R` is non-negative, then the point obtained by subtracting `p₁` from `x`, scaling the result by `t`, and then adding `p₂`, is weakly on the same side of the subspace `s` as `x`.
In mathematical terms, this theorem is essentially saying that if `p₁` and `p₂` are points in an affine subspace `s`, then any point along the line segment from `x` to `p₁`, translated by `p₂`, is weakly on the same side of `s` as `x`.
More concisely: For any strict ordered commutative ring R, additive commutative group V, R-module V, additive torsor P over V, affine subspace s of P, and points p₁, p₂ in s and x in P, if t is a non-negative scalar in R, then the point (x - p₁ + p₂) is weakly on the same side of s as x.
|
AffineSubspace.WSameSide.symm
theorem AffineSubspace.WSameSide.symm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : StrictOrderedCommRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {x y : P},
s.WSameSide x y → s.WSameSide y x
The theorem `AffineSubspace.WSameSide.symm` states that for any strict ordered commutative ring `R`, any additive commutative group `V`, any module `R` over `V`, and any affine torsor `P` over `V`, if the points `x` and `y` are weakly on the same side of an affine subspace `s` (`AffineSubspace.WSameSide s x y`), then the points `y` and `x` are also weakly on the same side of the same affine subspace (`AffineSubspace.WSameSide s y x`).
The "weakly on the same side" condition here means that there exist points `p₁` and `p₂` in the subspace `s` such that the vectors `x -ᵥ p₁` and `y -ᵥ p₂` point in the same or opposite directions (they are on the "same ray").
More concisely: If points `x` and `y` are weakly on the same side of an affine subspace `s` in a commutative ring `R` with an additive commutative group `V` and a module `R` over `V`, then `y` and `x` are also weakly on the same side of `s`.
|
AffineSubspace.wOppSide_comm
theorem AffineSubspace.wOppSide_comm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : StrictOrderedCommRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {x y : P},
s.WOppSide x y ↔ s.WOppSide y x
This theorem states that for any strict ordered commutative ring `R`, additive commutative group `V`, module `R` over `V`, and an additive torsor `P` over `V`, with `s` being an affine subspace of `P`, and `x` and `y` being two points in `P`, the property of `x` and `y` being weakly on the opposite sides of subspace `s` is commutative. That is, `x` being weakly on the opposite side of `s` from `y` is logically equivalent to `y` being weakly on the opposite side of `s` from `x`.
Remember that `x` and `y` are said to be weakly on the opposite sides of `s` if there exists two points `p₁` and `p₂` in `s` such that the subtracted vectors `(x -ᵥ p₁)` and `(p₂ -ᵥ y)` are on the same ray in the `R`-vector space `V`.
More concisely: For any strict ordered commutative ring `R`, additive commutative group `V`, `R`-module `P` over `V`, and an additive torsor `P` over `V`, with `s` being an affine subspace of `P`, the property of two points `x` and `y` in `P` being weakly on opposite sides of `s` is a symmetric relation.
|
AffineSubspace.wSameSide_comm
theorem AffineSubspace.wSameSide_comm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : StrictOrderedCommRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {x y : P},
s.WSameSide x y ↔ s.WSameSide y x
The theorem `AffineSubspace.wSameSide_comm` states that for any given strict ordered commutative ring `R`, an additive commutative group `V`, a module `R` of `V`, an additive torsor `V` of `P`, an affine subspace `s` of `P`, and two points `x` and `y` in `P`, the property of `x` and `y` being weakly on the same side of `s` is commutative. In other words, `x` and `y` are weakly on the same side of `s` if and only if `y` and `x` are weakly on the same side of `s`. Here, being weakly on the same side means that there exists two points in the subspace such that the vectors from these points to `x` and `y` respectively are in the same direction or opposite directions.
More concisely: For any strict ordered commutative ring R, additive commutative group V, R-module V, additive torsor V over a point P, affine subspace s of P, and points x and y in P, x and y are weakly on the same side of s if and only if y and x are weakly on the same side of s.
|
AffineSubspace.wOppSide_smul_vsub_vadd_left
theorem AffineSubspace.wOppSide_smul_vsub_vadd_left :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : StrictOrderedCommRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {s : AffineSubspace R P} {p₁ p₂ : P} (x : P),
p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, t ≤ 0 → s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x
The theorem `AffineSubspace.wOppSide_smul_vsub_vadd_left` states that for any strict ordered commutative ring `R`, add commutative group `V`, and an affine space `P` over `V`, given an affine subspace `s` of `P`, points `p₁` and `p₂` in `s`, and a point `x` in `P`, if a scalar `t` is less than or equal to zero, then the point obtained by scaling the affine difference of `x` and `p₁` by `t` and then translating by `p₂`, is weakly on the opposite side of subspace `s` relative to `x`. In mathematical terms, the theorem indicates that if `p₁` and `p₂` are points in the subspace, then the point `t • (x - p₁) + p₂` is on the weak opposite side of the subspace from `x` when `t` is less than or equal to zero.
More concisely: For any affine subspace `s` of an affine space `P` over a commutative ring `R` with identity, points `p₁, p₂ ∈ s`, and `x ∈ P`, if `t ≤ 0` then `t • (x - p₁) + p₂` is weakly opposite to `x` with respect to `s`.
|