iUnion_connectedComponentSupp — Mathlib

English

The union of all component supports equals the entire vertex set.

Русский

Объединение поддержек всех компонент равно множеству вершин графа.

LaTeX

$$$ \\bigcup_{c : G.ConnectedComponent} c.supp = \\mathrm{Set.univ} $$$

Lean4

theorem iUnion_connectedComponentSupp (G : SimpleGraph V) : ⋃ c : G.ConnectedComponent, c.supp = Set.univ :=
  by
  refine Set.eq_univ_of_forall fun v ↦ ⟨G.connectedComponentMk v, ?_⟩
  simp only [Set.mem_range, SetLike.mem_coe]
  exact ⟨⟨G.connectedComponentMk v, rfl⟩, rfl⟩

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