Betweenness in affine spaces for strictly convex spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[normed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
[strict_convex_space ℝ V]
(p : P)
{p₁ p₂ p₃ : P}
(h : sbtw ℝ p₁ p₂ p₃) :
has_dist.dist p₂ p < linear_order.max (has_dist.dist p₁ p) (has_dist.dist p₃ p)
theorem
wbtw.dist_le_max_dist
{V : Type u_1}
{P : Type u_2}
[normed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
[strict_convex_space ℝ V]
(p : P)
{p₁ p₂ p₃ : P}
(h : wbtw ℝ p₁ p₂ p₃) :
has_dist.dist p₂ p ≤ linear_order.max (has_dist.dist p₁ p) (has_dist.dist p₃ p)
theorem
collinear.wbtw_of_dist_eq_of_dist_le
{V : Type u_1}
{P : Type u_2}
[normed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
[strict_convex_space ℝ V]
{p p₁ p₂ p₃ : P}
{r : ℝ}
(h : collinear ℝ {p₁, p₂, p₃})
(hp₁ : has_dist.dist p₁ p = r)
(hp₂ : has_dist.dist p₂ p ≤ r)
(hp₃ : has_dist.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}
[normed_add_comm_group V]
[normed_space ℝ V]
[pseudo_metric_space P]
[normed_add_torsor V P]
[strict_convex_space ℝ V]
{p p₁ p₂ p₃ : P}
{r : ℝ}
(h : collinear ℝ {p₁, p₂, p₃})
(hp₁ : has_dist.dist p₁ p = r)
(hp₂ : has_dist.dist p₂ p < r)
(hp₃ : has_dist.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.