cospherical_def — Mathlib

English

Cospherical ps is defined by the existence of a center and a radius with all points at that distance from the center.

Русский

Определение косферического множества: существует центр и радиус с тем свойством, что все точки на этом расстоянии от центра.

LaTeX

$$$$ Cospherical(ps) \iff \exists c \in P, \exists r \in \mathbb{R}, \forall p \in ps, \operatorname{dist}(p,c) = r. $$$$

Lean4

/-- The definition of `Cospherical`. -/
theorem cospherical_def (ps : Set P) : Cospherical ps ↔ ∃ (center : P) (radius : ℝ), ∀ p ∈ ps, dist p center = radius :=
  Iff.rfl

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