midpoint_self
theorem midpoint_self :
∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] [inst_4 : AddTorsor V P] (x : P), midpoint R x x = x
The theorem `midpoint_self` states that for any point `x` in an affine space `P`, which is associated with a vector space `V` over a ring `R`, the midpoint of the segment from `x` to `x` itself is `x`. This is a mathematical way of saying that the midpoint of a line segment with the same start and end points is just the point itself. This holds true for any ring `R` where `2` is invertible, any additive commutative group `V`, any `R`-module structure on `V`, and any affine torsor `P` over `V`.
More concisely: For any point `x` in an affine space `P` over a ring `R` where 2 is invertible, the midpoint of the segment from `x` to `x` is `x`.
|
midpoint_eq_smul_add
theorem midpoint_eq_smul_add :
∀ (R : Type u_1) {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] (x y : V), midpoint R x y = ⅟2 • (x + y)
The theorem `midpoint_eq_smul_add` states that for any Ring `R`, and for any vectors `x` and `y` in an additive commutative group `V` that is also a module over `R`, the midpoint between `x` and `y` is equal to half the sum of `x` and `y`. In other words, the midpoint of two vectors is the scaled sum of the vectors, with the scale factor being the multiplicative inverse of 2. This theorem essentially formalizes the typical understanding of the "midpoint" of two points in a vector space.
More concisely: For any additive commutative group `V` that is an `R`-module, and for all vectors `x` and `y` in `V` over a ring `R`, the midpoint of `x` and `y` is equal to (1/2) * (x + y).
|
left_vsub_midpoint
theorem left_vsub_midpoint :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ : P), p₁ -ᵥ midpoint R p₁ p₂ = ⅟2 • (p₁ -ᵥ p₂)
This theorem, named `left_vsub_midpoint`, states that for any ring `R`, an additive commutative group `V`, an `R`-module structure on `V`, and an additive torsor `P` over `V`, and for any two points `p₁` and `p₂` in `P`, the difference between `p₁` and the midpoint of `p₁` and `p₂` is half of the difference between `p₁` and `p₂`. Here, `-ᵥ` represents the difference between two points in `P`, and `•` represents the scalar multiplication in the `R`-module `V`. The `⅟2` is the multiplicative inverse of `2` in the ring `R`, assuming `2` is invertible in `R`.
More concisely: For any additive torsor `P` over an `R`-module `V` with midpoint `m`, and for any two points `p₁, p₂` in `P`, the difference `p₁ - m` equals half the difference `(p₁ - p₂)` if `R` has an invertible element `2`.
|
AffineEquiv.pointReflection_midpoint_left
theorem AffineEquiv.pointReflection_midpoint_left :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P),
(AffineEquiv.pointReflection R (midpoint R x y)) x = y
This theorem states that for any ring `R`, additive commutative group `V`, and affine torsor `P` with `V` acting on `P`, and for any points `x` and `y` in `P`, the point reflection in the midpoint of `x` and `y` maps `x` to `y`. In other words, if you imagine a line segment with endpoints `x` and `y`, and reflect point `x` across the midpoint of this segment, you will end up at `y`.
More concisely: For any additive commutative group `V`, ring `R`, and affine torsor `P` over `R` with `V` acting on `P`, the reflection of a point `x` in the midpoint of the line segment between `x` and any other point `y` in `P` equals `y`.
|
midpoint_unique
theorem midpoint_unique :
∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] [inst_4 : AddTorsor V P] (R' : Type u_6) [inst_5 : Ring R'] [inst_6 : Invertible 2]
[inst_7 : Module R' V] (x y : P), midpoint R x y = midpoint R' x y
The theorem `midpoint_unique` states that the `midpoint` function, which calculates the midpoint of a segment `[x, y]` in a vector space or affine space, does not depend on the choice of the ring `R` over which the space is defined. In other words, if you have two rings `R` and `R'` and the same points `x` and `y`, the midpoint of `x` and `y` calculated over `R` is the same as the midpoint calculated over `R'`.
More concisely: Given rings R and R', and points x and y in a vector or affine space, the midpoint of the segment [x, y] is the same in R and R'.
|
midpoint_eq_iff
theorem midpoint_eq_iff :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P},
midpoint R x y = z ↔ (AffineEquiv.pointReflection R z) x = y
This theorem states that for any points `x`, `y`, and `z` in an affine space `P`, over a ring `R` with an additive commutative group `V` acting on it as a torsor, `z` is the midpoint of `x` and `y` if and only if reflecting `x` across `z` gives `y`. In other words, `z` bisects the line segment between `x` and `y` if `x` and `y` are symmetric about `z`.
More concisely: Given an affine space P over a ring R with an additive commutative group V acting as a torsor, point x, y, and z in P such that reflecting x across z results in y, then z is the midpoint of the line segment between x and y.
|
midpoint_vadd_midpoint
theorem midpoint_vadd_midpoint :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] [inst_4 : AddTorsor V P] (v v' : V) (p p' : P),
midpoint R v v' +ᵥ midpoint R p p' = midpoint R (v +ᵥ p) (v' +ᵥ p')
The theorem `midpoint_vadd_midpoint` states that for any ring `R`, invertible element 2, additive commutative group `V`, module `R` over `V`, additive torsor `V` over `P`, and any elements `v`, `v'` in `V` and `p`, `p'` in `P`, the sum of the midpoints of `v` and `v'`, and `p` and `p'` respectively (defined in a vector space), is equal to the midpoint of the sum of `v` and `p`, and `v'` and `p'`. In mathematical terms, this can be expressed as:
For all v, v' in V and p, p' in P, Midpoint(v, v') + Midpoint(p, p') = Midpoint(v+p, v'+p').
This theorem relates the operations of vector addition and finding midpoints in a certain way.
More concisely: For any additive torsors `V` over a group `P` in a commutative ring `R` with invertible element 2, the midpoints of the vector sum and the midpoints of the corresponding elements in `V` and `P` are equal. In other words, Midpoint(v+p, v'+p') = Midpoint(v, v') + Midpoint(p, p') for all `v`, `v'` in `V` and `p`, `p'` in `P`.
|
midpoint_vsub_left
theorem midpoint_vsub_left :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ : P), midpoint R p₁ p₂ -ᵥ p₁ = ⅟2 • (p₂ -ᵥ p₁)
The theorem `midpoint_vsub_left` is a statement about midpoints in a vector space over a ring. Given any two points `p₁` and `p₂` in an affine space with associated vector space `V` over a ring `R` where `2` is invertible, the vector obtained by subtracting `p₁` from the midpoint of `p₁` and `p₂` is equal to half of the vector obtained by subtracting `p₁` from `p₂`. In mathematical terms, this is saying that the vector from `p₁` to the midpoint of `p₁` and `p₂` is half of the vector from `p₁` to `p₂`, i.e., if `M` is the midpoint of `[p₁, p₂]`, then `→p₁M = ½•→p₁p₂`.
More concisely: Given any two points in an affine space over a ring where 2 is invertible, the vector from the first point to the midpoint of the two points is equal to half the vector from the first point to the second point.
|
midpoint_comm
theorem midpoint_comm :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), midpoint R x y = midpoint R y x
The theorem `midpoint_comm` states that for all types `R`, `V`, and `P`, with `R` being a ring, `2` being invertible, `V` being an additive commutative group, `R` being a module over `V`, and `V` being an additive torsor over `P`, the midpoint of two points `x` and `y` in the space `P` is the same as the midpoint of `y` and `x`. This means that the operation of taking the midpoint is commutative. In other words, swapping the positions of `x` and `y` does not change the result of the midpoint operation.
More concisely: For all types `R`, `V`, `P` (with `R` a ring, `2` invertible, `V` an additive commutative group, `R` an `R`-module over `V`, and `V` an additive torsor over `P`), the midpoint of `x` and `y` in `P` is equal to the midpoint of `y` and `x`.
|
midpoint_vsub_midpoint
theorem midpoint_vsub_midpoint :
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
[inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ p₃ p₄ : P),
midpoint R p₁ p₂ -ᵥ midpoint R p₃ p₄ = midpoint R (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)
The theorem `midpoint_vsub_midpoint` states that for any ring `R`, an additive commutative group `V`, a module structure between `R` and `V`, an additive torsor `P` over `V`, and any four points `p₁, p₂, p₃, p₄` in `P`, the difference vector between the midpoint of `p₁` and `p₂` and the midpoint of `p₃` and `p₄` is equal to the midpoint of the difference vectors `p₁ -ᵥ p₃` and `p₂ -ᵥ p₄`. Essentially, this theorem captures a geometric property about midpoints and difference vectors in the context of affine spaces.
More concisely: For any additive commutative group `V` with an `R`-module structure, an additive torsor `P` over `V`, and points `p₁, p₂, p₃, p₄` in `P`, the midpoint of `(p₁ + p₂) / 2` and `(p₃ + p₄) / 2` equals `(p₁ - p₃ + p₂ - p₄) / 2`.
|