ediam_eq_one — Mathlib

English

A graph has ediam = 1 if and only if it is the top graph (complete).

Русский

Граф имеет ediam = 1 тогда и только тогда, когда он является верхним графом (полным).

LaTeX

$$$$ G.ediam = 1 \\iff G = \\top $$$$

Lean4

@[simp]
theorem ediam_eq_one [Nontrivial α] : G.ediam = 1 ↔ G = ⊤ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ediam_top⟩
  rw [eq_top_iff_forall_eccent_eq_one]
  intro u
  apply le_antisymm (h ▸ eccent_le_ediam)
  rw [Order.one_le_iff_pos, pos_iff_ne_zero]
  exact eccent_ne_zero u

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