circumradius_pos — Mathlib

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

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