center_eq_iff_eq_of_mem — Mathlib

English

If p lies in both spheres, then equality of centers is equivalent to equality of the spheres.

Русский

Если точка принадлежит обеим сферам, то равенство центров эквивалентно равенству сфер.

LaTeX

$$$$ p \in s_1 \quad\text{и}\quad p \in s_2 \Rightarrow (s_1.center = s_2.center \iff s_1 = s_2). $$$$

Lean4

theorem center_eq_iff_eq_of_mem {s₁ s₂ : Sphere P} {p : P} (hs₁ : p ∈ s₁) (hs₂ : p ∈ s₂) :
    s₁.center = s₂.center ↔ s₁ = s₂ :=
  by
  refine ⟨fun h => Sphere.ext h ?_, fun h => h ▸ rfl⟩
  rw [mem_sphere] at hs₁ hs₂
  rw [← hs₁, ← hs₂, h]

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