top_supp_eq_univ — Mathlib

English

For a connected component of the top graph ⊤ on V, its support is the entire vertex set V.

Русский

Для компоненты связности графа верхнего уровня ⊤ на V опора равна всему множеству вершин V.

LaTeX

$$$c.supp = \\mathrm{Set.univ}$$$

Lean4

theorem top_supp_eq_univ (c : ConnectedComponent (⊤ : SimpleGraph V)) : c.supp = (Set.univ : Set V) :=
  by
  obtain ⟨w, rfl⟩ := c.exists_rep
  ext v
  simpa [-ConnectedComponent.eq] using ConnectedComponent.sound (G := ⊤)

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