eccent_top — Mathlib

English

In the complete graph on α, every vertex has eccentricity equal to 1.

Русский

В полном графе на α экцентриситет каждой вершины равен 1.

LaTeX

$$ (⊤ : SimpleGraph α).eccent u = 1$$

Lean4

@[simp]
theorem eccent_top [Nontrivial α] (u : α) : (⊤ : SimpleGraph α).eccent u = 1 :=
  by
  apply le_antisymm ?_ <| Order.one_le_iff_pos.mpr <| pos_iff_ne_zero.mpr <| eccent_ne_zero u
  rw [eccent, iSup_le_iff]
  intro v
  cases eq_or_ne u v <;> simp_all [edist_top_of_ne]

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