dist_lineMap_left
theorem dist_lineMap_left :
โ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] {๐ : Type u_6} [inst_3 : NormedField ๐] [inst_4 : NormedSpace ๐ V] (pโ pโ : P)
(c : ๐), dist ((AffineMap.lineMap pโ pโ) c) pโ = โcโ * dist pโ pโ
The theorem `dist_lineMap_left` states that for all points `pโ` and `pโ` in a pseudometric space `P` that is also a normed add-torsor over a seminormed add-commutative group `V`, and for all scalars `c` in a normed field `๐` that is also a normed space over `V`, the distance from the point mapped from `c` by the affine map from `๐` to `P` sending `0` to `pโ` and `1` to `pโ` to `pโ` is equal to the product of the norm of `c` and the distance from `pโ` to `pโ`. In mathematical terms, we have $dist( AffineMap.lineMap(pโ, pโ)(c), pโ) = โcโ * dist(pโ, pโ)$.
More concisely: The distance between the point in a normed add-torsor over a seminormed add-commutative group that is the image of a scalar under the affine map from the scalar field to the group, sending 0 to a point pโ and 1 to another point pโ, and pโ is equal to the product of the norm of the scalar and the distance between pโ and pโ.
|
dist_midpoint_right
theorem dist_midpoint_right :
โ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] {๐ : Type u_6} [inst_3 : NormedField ๐] [inst_4 : NormedSpace ๐ V]
[inst_5 : Invertible 2] (pโ pโ : P), dist (midpoint ๐ pโ pโ) pโ = โ2โโปยน * dist pโ pโ
The theorem `dist_midpoint_right` states that for any two points `pโ` and `pโ` in a pseudo-metric space `P` with an associated seminormed add commutative group `V`, the distance from the midpoint of `pโ` and `pโ` to `pโ` is equal to the inverse of the norm of 2 times the distance from `pโ` to `pโ`. Here the space `P` is a normed add-torsor over `V`, `V` is a normed space over a normed field `๐`, and 2 is invertible. In mathematical notation, this is saying that $dist(midpoint(pโ, pโ), pโ) = โ2โโปยน * dist(pโ, pโ)$.
More concisely: In a normed add-torsor P over a normed space V with invertible 2, the midpoint distance to V's additive inverse is equal to the reciprocal of twice the distance between the two points. ($dist(midpoint(pโ, pโ), -pโ) = โ2โโปยน * dist(pโ, pโ)$)
|
dist_lineMap_right
theorem dist_lineMap_right :
โ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] {๐ : Type u_6} [inst_3 : NormedField ๐] [inst_4 : NormedSpace ๐ V] (pโ pโ : P)
(c : ๐), dist ((AffineMap.lineMap pโ pโ) c) pโ = โ1 - cโ * dist pโ pโ
The theorem `dist_lineMap_right` states that for any two points `pโ` and `pโ` in a pseudo-metric space `P` with a seminormed add commutative group structure `V` and a normed add torsor structure, and for any scalar `c` from a normed field `๐`, the distance between the image of `c` under the affine map from `๐` to `P` sending `0` to `pโ` and `1` to `pโ` and the point `pโ` equals the absolute value of `(1 - c)` times the distance between `pโ` and `pโ`. This means that the distance from any point `c` on the line segment between `pโ` and `pโ` to `pโ` scales linearly with the distance between `pโ` and `pโ` and the deviation of `c` from `1`.
More concisely: Given a pseudo-metric space with a seminormed add commutative group structure and a normed add torsor structure, the distance from a point on the line segment between two points to the second point is proportional to the difference between 1 and the scalar representing the point, multiplied by the distance between the two points.
|
dist_left_midpoint
theorem dist_left_midpoint :
โ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] {๐ : Type u_6} [inst_3 : NormedField ๐] [inst_4 : NormedSpace ๐ V]
[inst_5 : Invertible 2] (pโ pโ : P), dist pโ (midpoint ๐ pโ pโ) = โ2โโปยน * dist pโ pโ
The theorem `dist_left_midpoint` states that for any points `pโ` and `pโ` in a pseudo-metric space `P`, which is also a normed add-torsor over a seminormed add-commutative group `V` (meaning that we can measure the distance between points and add displacements in `P`), and `V` is a normed space over a normed field `๐`, the distance between `pโ` and the midpoint between `pโ` and `pโ` is equal to the inverse of the norm of 2 multiplied by the distance between `pโ` and `pโ`. This essentially tells us that the midpoint is exactly half the distance away from either endpoint in a normed space.
More concisely: In a pseudometric space that is a normed add-torsor over a normed semigroup in a normed field, the distance from a point to the midpoint of two points is equal to the constant 1/2 multiplied by the distance between the two points.
|
dist_midpoint_left
theorem dist_midpoint_left :
โ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] {๐ : Type u_6} [inst_3 : NormedField ๐] [inst_4 : NormedSpace ๐ V]
[inst_5 : Invertible 2] (pโ pโ : P), dist (midpoint ๐ pโ pโ) pโ = โ2โโปยน * dist pโ pโ
The theorem `dist_midpoint_left` states that for all types `V`, `P`, and `๐` where `V` is a semi-normed add commutative group, `P` is a pseudo metric space, `V` is a normed add torsor over `P`, `๐` is a normed field, and `V` is a normed space over `๐`, and for all points `pโ` and `pโ` of type `P`, the distance between the midpoint of `pโ` and `pโ` and `pโ` is equal to the inverse of the norm of `2` multiplied by the distance between `pโ` and `pโ`. In mathematical notation, if $m$ is the midpoint of points $pโ$ and $pโ$, this can be written as $dist(m, pโ) = \frac{1}{\|2\|} * dist(pโ, pโ)$.
More concisely: The midpoint of two points in a normed add torsor over a pseudo metric space, where the underlying vector space is a normed space over a normed field, satisfies the property that the distance from the midpoint to one of the original points is equal to half the distance between the two original points, divided by the norm of 2.
|
dist_lineMap_lineMap
theorem dist_lineMap_lineMap :
โ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
[inst_2 : NormedAddTorsor V P] {๐ : Type u_6} [inst_3 : NormedField ๐] [inst_4 : NormedSpace ๐ V] (pโ pโ : P)
(cโ cโ : ๐), dist ((AffineMap.lineMap pโ pโ) cโ) ((AffineMap.lineMap pโ pโ) cโ) = dist cโ cโ * dist pโ pโ
This theorem states that for any pseudo metric space `P`, seminormed add commutative group `V`, normed add torsor `V P`, normed field `๐`, normed space `๐ V`, and given points `pโ` and `pโ` in `P`, and scalars `cโ` and `cโ` in `๐`, the distance between the points obtained by applying the affine map `AffineMap.lineMap pโ pโ` to `cโ` and `cโ` is equal to the product of the distance between `cโ` and `cโ` and the distance between `pโ` and `pโ`. In other words, the relative distances along the line between `pโ` and `pโ` created by the affine map are preserved.
More concisely: For any pseudo metric space `P`, seminormed add commutative group `V`, normed add torsor `V P`, normed field `๐`, normed space `๐ V`, and points `pโ, pโ in P` and scalars `cโ, cโ in ๐`, the distance between `AffineMap.lineMap pโ pโ cโ` and `AffineMap.lineMap pโ pโ cโ` is equal to the product of the distance between `cโ` and `cโ` and the distance between `pโ` and `pโ`.
|