eccent_eq_top_of_not_connected — Mathlib

English

If the graph is not connected, then the eccentricity of any vertex equals the top element ⊤.

Русский

Если граф не связный, eccent(u) = ⊤ для любого узла u.

LaTeX

$$¬ G.Connected → ∀ u, G.eccent u = ⊤$$

Lean4

theorem eccent_eq_top_of_not_connected (h : ¬G.Connected) (u : α) : G.eccent u = ⊤ :=
  by
  rw [connected_iff_exists_forall_reachable] at h
  push_neg at h
  obtain ⟨v, h⟩ := h u
  rw [eq_top_iff, ← edist_eq_top_of_not_reachable h]
  exact le_iSup (G.edist u) v

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