ediam_ne_zero — Mathlib

English

Let α be a nontrivial type and G a SimpleGraph on α. Then the ediam of G is not zero.

Русский

Пусть α ненулевого размера и G — простой граф на α. Тогда ediam(G) не равно 0.

LaTeX

$$$ \\forall \\alpha\\, \\forall G:\\text{ SimpleGraph }\\alpha\\,\\ [\\text{Nontrivial }\\alpha]\\Rightarrow G.ediam \\neq 0$$$

Lean4

theorem ediam_ne_zero [Nontrivial α] : G.ediam ≠ 0 :=
  by
  obtain ⟨u, v, huv⟩ := exists_pair_ne ‹_›
  contrapose! huv
  simp only [ediam, eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv
  exact huv u v

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