radius_eq_zero_iff — Mathlib

English

Radius is zero exactly when the vertex set is nonempty and subsingleton.

Русский

Радиус равен нулю тогда, когда множество вершин непусто и является одиночным.

LaTeX

$$$$ G.radius = 0 \iff (\mathrm{Nonempty}(\alpha) \wedge \mathrm{Subsingleton}(\alpha)). $$$$

Lean4

theorem radius_eq_zero_iff : G.radius = 0 ↔ Nonempty α ∧ Subsingleton α :=
  by
  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨_, _⟩ ↦ ?_⟩
  · contrapose! h
    simp [radius]
  · contrapose! h
    simp [radius_ne_zero_of_nontrivial]
  · rw [radius, ENat.iInf_eq_zero]
    use Classical.ofNonempty
    simpa [eccent] using Subsingleton.elim _

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