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]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
[StrictConvexSpace ℝ V]
(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]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
[StrictConvexSpace ℝ V]
(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]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
[StrictConvexSpace ℝ V]
{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]
[PseudoMetricSpace P]
[NormedAddTorsor V P]
[StrictConvexSpace ℝ V]
{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.