sbtw_of_collinear_of_dist_center_lt_radius

English

If three collinear points lie with two on a sphere and the middle point lies strictly between, then the middle point is strictly between them.

Русский

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

LaTeX

$$Sbtw ℝ p1 p2 p3$$

Lean4

/-- Given three collinear points, two on a sphere and one inside it, the one inside it is
strictly between the other two points. -/
theorem sbtw_of_collinear_of_dist_center_lt_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₃) : Sbtw ℝ p₁ p₂ p₃ :=
  h.sbtw_of_dist_eq_of_dist_lt hp₁ hp₂ hp₃ hp₁p₃

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