radius_ne_zero_of_nontrivial — Mathlib

English

If α is nontrivial, then G.radius ≠ 0.

Русский

Если множество вершин не тривиально, то радиус графа не равен нулю.

LaTeX

$$$$ \forall {\alpha}, \forall G:\mathrm{SimpleGraph}(\alpha), [\mathrm{Nontrivial}(\alpha)] \Rightarrow G.radius \neq 0. $$$$

Lean4

theorem radius_ne_zero_of_nontrivial [Nontrivial α] : G.radius ≠ 0 :=
  by
  rw [← ENat.one_le_iff_ne_zero]
  apply le_iInf
  simp [ENat.one_le_iff_ne_zero, G.eccent_ne_zero]

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