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