English
If the simplex has at least two points, then its circumradius is strictly positive.
Русский
Если у многогранника по крайней мере две вершины, циркумрадиус положителен.
LaTeX
$$$ s.circumradius > 0$ for $n+1$-simplex with at least two vertices.$$
Lean4
/-- The circumradius of a simplex with at least two points is
positive. -/
theorem circumradius_pos {n : ℕ} (s : Simplex ℝ P (n + 1)) : 0 < s.circumradius :=
by
refine lt_of_le_of_ne s.circumradius_nonneg ?_
intro h
have hr := s.dist_circumcenter_eq_circumradius
simp_rw [← h, dist_eq_zero] at hr
have h01 := s.independent.injective.ne (by simp : (0 : Fin (n + 2)) ≠ 1)
simp [hr] at h01