center_ne_iff_ne_of_mem — Mathlib

English

If p lies in both spheres, then center inequality is equivalent to sphere inequality.

Русский

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

LaTeX

$$$$ p \in s_1 \land p \in s_2 \Rightarrow (s_1.center \neq s_2.center \iff s_1 \neq s_2). $$$$

Lean4

theorem center_ne_iff_ne_of_mem {s₁ s₂ : Sphere P} {p : P} (hs₁ : p ∈ s₁) (hs₂ : p ∈ s₂) :
    s₁.center ≠ s₂.center ↔ s₁ ≠ s₂ :=
  (Sphere.center_eq_iff_eq_of_mem hs₁ hs₂).not

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