dist_circumcenter_eq_circumradius'

English

For a simplex s, the circumsphere is the unique sphere containing all vertices with its center in the affine span of the vertices.

Русский

Для простейшего многообразия circumsphere есть единственная сфера, содержащая все вершины и центр которой лежит в афинном охвате вершин.

LaTeX

$$$(s.circumsphere)\\;\\text{is unique with }\\text{center} \\in affineSpan ℝ (Set.range s.points) \\land Set.range s.points \\subset s.circumsphere$$$

Lean4

/-- All points have distance to the circumcenter equal to the
circumradius. -/
@[simp]
theorem dist_circumcenter_eq_circumradius' {n : ℕ} (s : Simplex ℝ P n) :
    ∀ i, dist s.circumcenter (s.points i) = s.circumradius :=
  by
  intro i
  rw [dist_comm]
  exact dist_circumcenter_eq_circumradius _ _

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