Betweenness in affine spaces for strictly convex spaces #
This file proves results about betweenness for points in an affine space for a strictly convex space.
theorem
Sbtw.dist_lt_max_dist
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[StrictConvexSpace ℝ V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
{p₁ : P}
{p₂ : P}
{p₃ : P}
(h : Sbtw ℝ p₁ p₂ p₃)
:
theorem
Wbtw.dist_le_max_dist
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[StrictConvexSpace ℝ V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
(p : P)
{p₁ : P}
{p₂ : P}
{p₃ : P}
(h : Wbtw ℝ p₁ p₂ p₃)
:
theorem
Collinear.wbtw_of_dist_eq_of_dist_le
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[StrictConvexSpace ℝ V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
{p : P}
{p₁ : P}
{p₂ : P}
{p₃ : P}
{r : ℝ}
(h : Collinear ℝ {p₁, p₂, p₃})
(hp₁ : dist p₁ p = r)
(hp₂ : dist p₂ p ≤ r)
(hp₃ : dist p₃ p = r)
(hp₁p₃ : p₁ ≠ p₃)
:
Given three collinear points, two (not equal) with distance r from p and one with
distance at most r from p, the third point is weakly between the other two points.
theorem
Collinear.sbtw_of_dist_eq_of_dist_lt
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[StrictConvexSpace ℝ V]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
{p : P}
{p₁ : P}
{p₂ : P}
{p₃ : P}
{r : ℝ}
(h : Collinear ℝ {p₁, p₂, p₃})
(hp₁ : dist p₁ p = r)
(hp₂ : dist p₂ p < r)
(hp₃ : dist p₃ p = r)
(hp₁p₃ : p₁ ≠ p₃)
:
Given three collinear points, two (not equal) with distance r from p and one with
distance less than r from p, the third point is strictly between the other two points.
theorem
dist_add_dist_eq_iff
{V : Type u_1}
{P : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[StrictConvexSpace ℝ V]
[MetricSpace P]
[NormedAddTorsor V P]
{a : P}
{b : P}
{c : P}
:
In a strictly convex space, the triangle inequality turns into an equality if and only if the middle point belongs to the segment joining two other points.
theorem
eq_lineMap_of_dist_eq_mul_of_dist_eq_mul
{E : Type u_3}
{PE : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[StrictConvexSpace ℝ E]
[MetricSpace PE]
[NormedAddTorsor E PE]
{r : ℝ}
{x : PE}
{y : PE}
{z : PE}
(hxy : dist x y = r * dist x z)
(hyz : dist y z = (1 - r) * dist x z)
:
y = (AffineMap.lineMap x z) r
theorem
eq_midpoint_of_dist_eq_half
{E : Type u_3}
{PE : Type u_5}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[StrictConvexSpace ℝ E]
[MetricSpace PE]
[NormedAddTorsor E PE]
{x : PE}
{y : PE}
{z : PE}
(hx : dist x y = dist x z / 2)
(hy : dist y z = dist x z / 2)
:
noncomputable def
Isometry.affineIsometryOfStrictConvexSpace
{E : Type u_3}
{F : Type u_4}
{PE : Type u_5}
{PF : Type u_6}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedSpace ℝ E]
[NormedSpace ℝ F]
[StrictConvexSpace ℝ E]
[MetricSpace PE]
[MetricSpace PF]
[NormedAddTorsor E PE]
[NormedAddTorsor F PF]
{f : PF → PE}
(hi : Isometry f)
:
An isometry of NormedAddTorsors for real normed spaces, strictly convex in the case of the
codomain, is an affine isometry. Unlike Mazur-Ulam, this does not require the isometry to be
surjective.
Equations
- Isometry.affineIsometryOfStrictConvexSpace hi = let __src := AffineMap.ofMapMidpoint f ⋯ ⋯; { toAffineMap := __src, norm_map := ⋯ }
Instances For
@[simp]
theorem
Isometry.coe_affineIsometryOfStrictConvexSpace
{E : Type u_3}
{F : Type u_4}
{PE : Type u_5}
{PF : Type u_6}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedSpace ℝ E]
[NormedSpace ℝ F]
[StrictConvexSpace ℝ E]
[MetricSpace PE]
[MetricSpace PF]
[NormedAddTorsor E PE]
[NormedAddTorsor F PF]
{f : PF → PE}
(hi : Isometry f)
:
@[simp]
theorem
Isometry.affineIsometryOfStrictConvexSpace_apply
{E : Type u_3}
{F : Type u_4}
{PE : Type u_5}
{PF : Type u_6}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedSpace ℝ E]
[NormedSpace ℝ F]
[StrictConvexSpace ℝ E]
[MetricSpace PE]
[MetricSpace PF]
[NormedAddTorsor E PE]
[NormedAddTorsor F PF]
{f : PF → PE}
(hi : Isometry f)
(p : PF)
:
(Isometry.affineIsometryOfStrictConvexSpace hi) p = f p