eq_top_iff_forall_eccent_eq_one — Mathlib

English

A graph G is equal to the top graph if and only if every vertex has eccentricity 1.

Русский

Граф G равен верхнему графу тогда, когда все вершины имеют экцентриситет 1.

LaTeX

$$G = ⊤ \iff ∀ u, G.eccent u = 1$$

Lean4

theorem eq_top_iff_forall_eccent_eq_one [Nontrivial α] : G = ⊤ ↔ ∀ u, G.eccent u = 1 :=
  by
  refine ⟨fun h ↦ h ▸ eccent_top, fun h ↦ ?_⟩
  ext u v
  refine ⟨Adj.ne, fun huv ↦ ?_⟩
  rw [← edist_eq_one_iff_adj]
  apply le_antisymm ((h u).symm ▸ edist_le_eccent)
  rw [Order.one_le_iff_pos, pos_iff_ne_zero, edist_eq_zero_iff.ne]
  exact huv.ne

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