sbtw_of_dist_eq_of_dist_lt — Mathlib

English

If the middle point lies strictly between two endpoints in a collinear configuration, then it is strictly between them.

Русский

Если середина между концами лежит строго между ними в коллинеарной конфигурации, то она строго между ними.

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)

Lean4

/-- 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 sbtw_of_dist_eq_of_dist_lt {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₃) : Sbtw ℝ p₁ p₂ p₃ :=
  by
  refine ⟨h.wbtw_of_dist_eq_of_dist_le hp₁ hp₂.le hp₃ hp₁p₃, ?_, ?_⟩
  · rintro rfl
    exact hp₂.ne hp₁
  · rintro rfl
    exact hp₂.ne hp₃

Похожие утверждения