English
Given three collinear points with two equal distances and one at most r, the middle point lies weakly between the endpoints.
Русский
Имея три коллинеарные точки и одинаковые расстояния между ними, третья точка лежит между концами.
LaTeX
$$$\forall p,p_1,p_2,p_3,\ Collinear ℝ \{p_1,p_2,p_3\} \rightarrow dist(p_1,p)=r \rightarrow dist(p_2,p) \le r \rightarrow dist(p_3,p)=r \rightarrow p_1 \neq p_3 \Rightarrow Wbtw ℝ p_1 p_2 p_3$$$
Lean4
/-- 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 wbtw_of_dist_eq_of_dist_le {p p₁ p₂ p₃ : P} {r : ℝ} (h : Collinear ℝ ({ p₁, p₂, p₃ } : Set P))
(hp₁ : dist p₁ p = r) (hp₂ : dist p₂ p ≤ r) (hp₃ : dist p₃ p = r) (hp₁p₃ : p₁ ≠ p₃) : Wbtw ℝ p₁ p₂ p₃ :=
by
rcases h.wbtw_or_wbtw_or_wbtw with (hw | hw | hw)
· exact hw
· by_cases hp₃p₂ : p₃ = p₂
· simp [hp₃p₂]
have hs : Sbtw ℝ p₂ p₃ p₁ := ⟨hw, hp₃p₂, hp₁p₃.symm⟩
have hs' := hs.dist_lt_max_dist p
rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, or_false] at hs'
exact False.elim (hp₂.not_gt hs')
· by_cases hp₁p₂ : p₁ = p₂
· simp [hp₁p₂]
have hs : Sbtw ℝ p₃ p₁ p₂ := ⟨hw, hp₁p₃, hp₁p₂⟩
have hs' := hs.dist_lt_max_dist p
rw [hp₁, hp₃, lt_max_iff, lt_self_iff_false, false_or] at hs'
exact False.elim (hp₂.not_gt hs')
