verts_sInf

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

The vertex set of the infimum is the intersection of vertex sets of the components.

Русский

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

LaTeX

$$$ (sInf s).verts = \\\\bigcap G' ∈ s, \\mathrm{verts}(G') $$$

Lean4

@[simp]
theorem verts_sInf (s : Set G.Subgraph) : (sInf s).verts = ⋂ G' ∈ s, verts G' :=
  rfl

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

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

Разделы

Аффилиация

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