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.
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.
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.
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.
The strict triangle inequality.
An isometry of NormedAddTorsor
s 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 = { toAffineMap := AffineMap.ofMapMidpoint f ⋯ ⋯, norm_map := ⋯ }