dist_circumcenter_eq_circumradius

English

For any vertex i of a simplex, the distance from the circumcenter to that vertex equals the circumradius.

Русский

Расстояние от circumcenter до любой вершины равно циркумрадиусу.

LaTeX

$$$\\forall i, \\operatorname{dist}(s.points i, s.circumcenter) = s.circumradius$$$

Lean4

/-- All points have distance from the circumcenter equal to the
circumradius. -/
@[simp]
theorem dist_circumcenter_eq_circumradius {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    dist (s.points i) s.circumcenter = s.circumradius :=
  dist_of_mem_subset_sphere (Set.mem_range_self _) s.circumsphere_unique_dist_eq.1.2

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