cospherical_iff_exists_sphere — Mathlib

English

A set is cospherical if and only if it lies inside some sphere.

Русский

Множество косферично тогда и только тогда, когда оно содержится внутри некоторой сферы.

LaTeX

$$$$ Cospherical(ps) \iff \exists s: Sphere(P), ps \subseteq (s : Set P). $$$$

Lean4

/-- A set of points is cospherical if and only if they lie in some sphere. -/
theorem cospherical_iff_exists_sphere {ps : Set P} : Cospherical ps ↔ ∃ s : Sphere P, ps ⊆ (s : Set P) :=
  by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rcases h with ⟨c, r, h⟩
    exact ⟨⟨c, r⟩, h⟩
  · rcases h with ⟨s, h⟩
    exact ⟨s.center, s.radius, h⟩

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