cospherical_iff_exists_mem_of_finiteDimensional

English

Two sets of points are cospherical if and only if there exists a center in the ambient subspace equidistant from all points in the set.

Русский

Два набора точек косферические тогда и только тогда, когда существует центр в окружающем подпространстве, расстояния от которого до всех точек набора равны.

LaTeX

$$$\text{Cospherical}(ps) \iff \exists c\in s,\; \exists r,\ \forall p\in ps,\; \operatorname{dist}(p,c)=r$$$

Lean4

/-- Given a nonempty affine subspace, whose direction is
finite-dimensional, that contains a set of points, those points are
cospherical if and only if they are equidistant from some point in
that subspace. -/
theorem cospherical_iff_exists_mem_of_finiteDimensional {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ s) [Nonempty s]
    [FiniteDimensional ℝ s.direction] : Cospherical ps ↔ ∃ center ∈ s, ∃ radius : ℝ, ∀ p ∈ ps, dist p center = radius :=
  cospherical_iff_exists_mem_of_complete h

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