wbtw_of_collinear_of_dist_center_le_radius

English

If three points are collinear with two on a sphere and the third not outside, the middle point is weakly between the other two.

Русский

Если три точки коллинеарны и две лежат на сфере, а третья внутри, средняя точка между двумя другими слабопосредована.

LaTeX

$$Wbtw ℝ p1 s.center p2$$

Lean4

/-- Given three collinear points, two on a sphere and one not outside it, the one not outside it
is weakly between the other two points. -/
theorem wbtw_of_collinear_of_dist_center_le_radius {s : Sphere P} {p₁ p₂ p₃ : P}
    (h : Collinear ℝ ({ p₁, p₂, p₃ } : Set P)) (hp₁ : p₁ ∈ s) (hp₂ : dist p₂ s.center ≤ s.radius) (hp₃ : p₃ ∈ s)
    (hp₁p₃ : p₁ ≠ p₃) : Wbtw ℝ p₁ p₂ p₃ :=
  h.wbtw_of_dist_eq_of_dist_le hp₁ hp₂ hp₃ hp₁p₃

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