Cospherical — Mathlib

English

A set is cospherical if there exists a center and a radius such that every point of the set has distance equal to the radius 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

/-- A set of points is cospherical if they are equidistant from some
point. In two dimensions, this is the same thing as being
concyclic. -/
def Cospherical (ps : Set P) : Prop :=
  ∃ (center : P) (radius : ℝ), ∀ p ∈ ps, dist p center = radius

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