# 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} [] [] [] (p : P) {p₁ : P} {p₂ : P} {p₃ : P} (h : Sbtw p₁ p₂ p₃) :
dist p₂ p < max (dist p₁ p) (dist p₃ p)
theorem Wbtw.dist_le_max_dist {V : Type u_1} {P : Type u_2} [] [] [] (p : P) {p₁ : P} {p₂ : P} {p₃ : P} (h : Wbtw p₁ p₂ p₃) :
dist p₂ p max (dist p₁ p) (dist p₃ p)
theorem Collinear.wbtw_of_dist_eq_of_dist_le {V : Type u_1} {P : Type u_2} [] [] [] {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₃) :
Wbtw 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} [] [] [] {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₃) :
Sbtw 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} [] [] [] [] {a : P} {b : P} {c : P} :
dist a b + dist b c = dist a c Wbtw a b c

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} [] [] [] [] {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 = () r
theorem eq_midpoint_of_dist_eq_half {E : Type u_3} {PE : Type u_5} [] [] [] [] {x : PE} {y : PE} {z : PE} (hx : dist x y = dist x z / 2) (hy : dist y z = dist x z / 2) :
y =
noncomputable def Isometry.affineIsometryOfStrictConvexSpace {E : Type u_3} {F : Type u_4} {PE : Type u_5} {PF : Type u_6} [] [] [] [] [] [] [] {f : PFPE} (hi : ) :

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
• hi.affineIsometryOfStrictConvexSpace = let __src := ; { 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} [] [] [] [] [] [] [] {f : PFPE} (hi : ) :
hi.affineIsometryOfStrictConvexSpace = f
@[simp]
theorem Isometry.affineIsometryOfStrictConvexSpace_apply {E : Type u_3} {F : Type u_4} {PE : Type u_5} {PF : Type u_6} [] [] [] [] [] [] [] {f : PFPE} (hi : ) (p : PF) :
hi.affineIsometryOfStrictConvexSpace p = f p