verts_inf

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

The vertex set of the infimum (intersection) of two subgraphs is the intersection of their vertex sets.

Русский

Множество вершин пересечения двух подграфов равно пересечению их множеств вершин.

LaTeX

$$$(G_1 \\sqcap G_2).verts = G_1.verts \\cap G_2.verts$$$

Lean4

@[simp]
theorem verts_inf (G₁ G₂ : G.Subgraph) : (G₁ ⊓ G₂).verts = G₁.verts ∩ G₂.verts :=
  rfl

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

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

Разделы

Аффилиация

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