cospherical_pair — Mathlib

English

Two points are cospherical.

Русский

Две точки косферичны.

LaTeX

$$$$ \text{Cospherical}(\{p_1, p_2\} : Set P). $$$$

Lean4

/-- Two points are cospherical. -/
theorem cospherical_pair (p₁ p₂ : P) : Cospherical ({ p₁, p₂ } : Set P) :=
  ⟨midpoint ℝ p₁ p₂, ‖(2 : ℝ)‖⁻¹ * dist p₁ p₂, by
    rintro p (rfl | rfl | _)
    · rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]
    · rw [dist_comm, dist_midpoint_right (𝕜 := ℝ)]⟩

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