circumsphere — Mathlib

English

The circumsphere of a simplex is the unique sphere passing through all its vertices.

Русский

Циркумсфера многогранника — это единственная сфера, проходящая через все вершины.

LaTeX

$$$\\text{circumsphere}(s)\\quad\\text{is the unique }S\\text{ with }\\mathrm{range}(s.points) \\subset S \\text{ and } \\operatorname{center}(S) \\in \\mathrm{affineSpan}(\\mathrm{range}(s.points)).$$$

Lean4

/-- The circumsphere of a simplex. -/
def circumsphere {n : ℕ} (s : Simplex ℝ P n) : Sphere P :=
  s.independent.existsUnique_dist_eq.choose

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