Mathlib.Analysis.Convex.Between._auxLemma.15
theorem Mathlib.Analysis.Convex.Between._auxLemma.15 :
∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] (x y : P), Wbtw R x x y = True
This theorem, `Mathlib.Analysis.Convex.Between._auxLemma.15`, states that for any ordered ring `R`, any additive commutative group `V`, any module `V` over `R`, and any torsor `P` for `V`, given two points `x` and `y` in `P`, `y` is weakly between `x` and `x` itself. In other words, the point `y` is located on the affine segment from `x` to `x`, which is the point `x` itself.
More concisely: For any torsor `P` over an additive commutative group `V` in an ordered ring `R`, any two points `x` and `y` in `P` satisfy `y ≤ x ∨ x ≤ y`.
|
Sbtw.left_ne
theorem Sbtw.left_ne :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {x y z : P}, Sbtw R x y z → x ≠ y
The theorem `Sbtw.left_ne` states that for any types `R`, `V`, and `P`, where `R` is an ordered ring, `V` is an additive commutative group, `R` is a module over `V`, and `V` is an additive torsor over `P`, given any three points `x`, `y`, `z` of type `P`, if `y` is strictly between `x` and `z` (as defined by the `Sbtw` property), then `x` is not equal to `y`. In other words, if a point is strictly between two other points, it cannot coincide with the first of those points.
More concisely: If `R` is an ordered ring, `V` is an additive commutative group with `R` as a module and `V` an additive torsor over some type `P`, then for any `x`, `y`, `z` in `P` with `y` strictly between `x` and `z`, we have `x ≠ y`.
|
Sbtw.right_ne
theorem Sbtw.right_ne :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {x y z : P}, Sbtw R x y z → z ≠ y
The theorem `Sbtw.right_ne` states that for any ordered ring `R`, an additive commutative group `V`, a module `R V`, and an additive torsor `V P`, if a point `y` is strictly between points `x` and `z` (as defined by `Sbtw R x y z`), then `z` is not equal to `y`. In other words, the point `y` being strictly between `x` and `z` implies that `z` and `y` are distinct points.
More concisely: For any ordered ring R, additive commutative group V, R-module R V, and additive torsor V over P, if x, y, z in V satisfy x < y < z in the order on V induced by R, then y ≠ z.
|
Wbtw.symm
theorem Wbtw.symm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {x y z : P}, Wbtw R x y z → Wbtw R z y x
The theorem `Wbtw.symm` states that for any three points `x`, `y`, and `z` in a torsor `P`, where `P` is an affine space over a vector space `V` which is a module over an ordered ring `R`, if `y` is weakly between `x` and `z`, then `y` is also weakly between `z` and `x`. In other words, the "weakly between" relation is symmetrical.
More concisely: For any points `x`, `y`, `z` in an affine space `P` over a vector space `V` as a module over an ordered ring `R`, if `y` is weakly between `x` and `z`, then `y` is also weakly between `z` and `x` (i.e., the weakly between relation is reflexive and symmetric).
|
Wbtw.collinear
theorem Wbtw.collinear :
∀ {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] {x y z : P}, Wbtw R x y z → Collinear R {x, y, z}
This theorem states that for any given types `R`, `V`, `P` where `R` is a linear ordered field, `V` is an additive commutative group, `P` is a type with a torsor structure over `V`, and given any three points `x`, `y`, `z` of type `P`, if `y` is weakly between `x` and `z` (that is, `y` belongs to the affine segment between `x` and `z`), then the set of points `{x,y,z}` is collinear. In other words, if `y` lies between `x` and `z`, then `x`, `y`, and `z` all lie on the same line.
More concisely: Given a linear ordered field `R`, an additive commutative group `V`, and a torsor `P` over `V`, if `y` is weakly between `x` and `z` in `P`, then `x`, `y`, and `z` are collinear points in `P`.
|
Sbtw.ne_left
theorem Sbtw.ne_left :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {x y z : P}, Sbtw R x y z → y ≠ x
This theorem, named `Sbtw.ne_left`, states that for any points `x`, `y`, and `z` in an affine space `P`, which is a vector space `V` over an ordered ring `R`, if `y` is strictly between `x` and `z` (as defined by the `Sbtw` function), then `y` is not equal to `x`. This is captured mathematically as: for all `x`, `y`, `z` in `P`, `Sbtw R x y z` implies `y ≠ x`.
More concisely: In an affine space over an ordered ring, if point `y` is strictly between points `x` and `z`, then `y` is distinct from `x`.
|
Sbtw.wbtw
theorem Sbtw.wbtw :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {x y z : P}, Sbtw R x y z → Wbtw R x y z
This theorem states that for any types `R`, `V`, `P` where `R` is an ordered ring, `V` is an additive commutative group, `P` is an affine space over `V` with `R` as its scalar field, and `x`, `y`, `z` are points in this affine space, if `y` is strictly between `x` and `z` (according to the definition `Sbtw`), then `y` is also weakly between `x` and `z` (according to the definition `Wbtw`). In other words, the condition of a point being strictly between two other points implies the condition of the point being weakly between the same two points.
More concisely: If `x`, `y`, `z` are points in an affine space over an ordered ring `R`, with `V` as its additive commutative group as the scalar field, and `y` is strictly between `x` and `z` (`Sbtw x y z`), then `y` is also weakly between `x` and `z` (`Wbtw x y z`).
|
sbtw_comm
theorem sbtw_comm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {x y z : P}, Sbtw R x y z ↔ Sbtw R z y x
This theorem, `sbtw_comm`, states that for any ordered ring `R`, additive commutative group `V`, module `R` over `V`, and an additive torsor `V` over `P`, the strict betweenness relation `Sbtw` is symmetric with respect to its endpoints. In other words, given any three points `x`, `y`, and `z` from `P`, the point `y` is strictly between `x` and `z` if and only if `y` is strictly between `z` and `x`.
More concisely: For any ordered ring R, additive commutative group V, R-module V, and additive torsor V over P, the strict betweenness relation Sbtw on P is a symmetric relation.
|
affineSegment_image
theorem affineSegment_image :
∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : OrderedRing R]
[inst_1 : AddCommGroup V] [inst_2 : Module R V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup V']
[inst_5 : Module R V'] [inst_6 : AddTorsor V' P'] (f : P →ᵃ[R] P') (x y : P),
⇑f '' affineSegment R x y = affineSegment R (f x) (f y)
This theorem states that for any affine transformation `f` from a point `P` to another point `P'`, the image of an affine segment between two points `x` and `y` under `f` is equivalent to the affine segment between the images of `x` and `y` under `f`. In other words, an affine transformation preserves the affine segments. Here, `P` and `P'` can be considered as points in vector spaces `V` and `V'` over the ordered ring `R`, respectively.
More concisely: Given affine transformations `f` from vector space `V` over ordered ring `R` and points `x, y` in `V`, the image of the affine segment `[x, y]` under `f` is equivalent to the affine segment `[fx, fy]`.
|
wbtw_comm
theorem wbtw_comm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {x y z : P}, Wbtw R x y z ↔ Wbtw R z y x
The theorem `wbtw_comm` states that for any ordered ring `R`, any additive commutative group `V`, any module `V` over `R`, any `V`-torsor `P`, and any three points `x`, `y`, and `z` in `P`, the property that `y` is weakly between `x` and `z` is equivalent to the property that `y` is weakly between `z` and `x`. In other words, the "weakly between" relation is symmetric: if `y` is on the line segment from `x` to `z` (inclusive), then `y` is also on the line segment from `z` to `x`.
More concisely: For any ordered ring `R`, additive commutative group `V` with a `R`-module structure, and `V`-torsor `P`, the relation "`y` is weakly between `x` and `z` in `P`" is equivalent to "`y` is weakly between `z` and `x` in `P`".
|
sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair
theorem sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : LinearOrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] [inst_4 : NoZeroSMulDivisors R V] {t : Affine.Triangle R P}
{i₁ i₂ i₃ : Fin 3},
i₁ ≠ i₂ →
∀ {p₁ p₂ p : P},
Sbtw R (t.points i₂) p₁ (t.points i₃) →
Sbtw R (t.points i₁) p₂ (t.points i₃) →
p ∈ affineSpan R {t.points i₁, p₁} → p ∈ affineSpan R {t.points i₂, p₂} → Sbtw R (t.points i₁) p p₁
This theorem states that given a triangle in an affine space over a field with a linear order and no zero divisors, if there are two lines from distinct vertices of the triangle to interior points of the opposite sides and these lines intersect at a point `p`, then `p` lies strictly between the vertex and the point on the opposite side. The theorem is symmetric, meaning it holds true for either segment from a vertex to the point on the opposite side.
More concisely: In an affine space over a field with a linear order and no zero divisors, if there are two lines from distinct vertices of a triangle to interior points of the opposite sides that intersect at a point, then this point lies strictly between the vertex and the point on the opposite side.
|
wbtw_swap_right_iff
theorem wbtw_swap_right_iff :
∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] [inst_4 : NoZeroSMulDivisors R V] (x : P) {y z : P},
Wbtw R x y z ∧ Wbtw R x z y ↔ y = z
The theorem `wbtw_swap_right_iff` states that for any ordered ring `R`, and given an additive commutative group `V`, a module `R V`, and an additive torsor `V P` where `P` is a type, and assuming `R V` has no zero scalar multipliers or divisors, for any points `x`, `y`, `z` of type `P`, the point `y` is weakly between `x` and `z` and the point `z` is weakly between `x` and `y` if and only if `y` is equal to `z`. In other words, it asserts that in the given algebraic structures, `y` and `z` can only both be weakly between `x` and each other if they are actually the same point.
More concisely: In an additive commutative group `V` over an ordered ring `R` with no zero scalar multipliers or divisors, two points `y` and `z` of type `P` are weakly between each other if and only if they are equal.
|
Sbtw.symm
theorem Sbtw.symm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {x y z : P}, Sbtw R x y z → Sbtw R z y x
The theorem `Sbtw.symm` states that for any ordered ring `R`, additive commutative group `V`, module `R V`, and an additively torsion-free module `V P`, and for any points `x`, `y`, and `z` of type `P`, if the point `y` is strictly between `x` and `z`, then the point `y` is also strictly between `z` and `x`. In other words, the "strictly between" relation is symmetric with respect to the points `x` and `z`.
More concisely: For any ordered ring R, additive commutative group V with module structure over R, and additively torsion-free module V over P, the strict between relation on points of P is symmetric: if x, y, z are points with y strictly between x and z, then y is also strictly between z and x.
|
Sbtw.ne_right
theorem Sbtw.ne_right :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : OrderedRing R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : AddTorsor V P] {x y z : P}, Sbtw R x y z → y ≠ z
The theorem `Sbtw.ne_right` states that for any ordered ring `R`, additive commutative group `V`, and additive torsor `P`, and for any points `x`, `y`, and `z` in `P`, if `y` is strictly between `x` and `z` (in the sense defined by `Sbtw`), then `y` is not equal to `z`.
More concisely: If `x`, `y`, and `z` are points in an additive torsor `P` over an ordered ring `R`, and `y` is strictly between `x` and `z`, then `y` is not equal to `z`.
|