verts_sSup

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.verts_sSup

English

The vertex set of the supremum is the union of vertex sets of the components.

Русский

Множество вершин наибольшего подграфа есть объединение множеств вершин компонентов.

LaTeX

$$$ (sSup s).verts = \\bigcup G' ∈ s, \\mathrm{verts}(G') $$$

Lean4

@[simp]
theorem verts_sSup (s : Set G.Subgraph) : (sSup s).verts = ⋃ G' ∈ s, verts G' :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru