verts_mono

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

If H ≤ H' then the vertex set of H is contained in the vertex set of H'.

Русский

Если H ≤ H', то вершинное множество H включено в вершины H'.

LaTeX

$$$ H \\le H' \\Rightarrow \\mathrm{verts}(H) \\subseteq \\mathrm{verts}(H') $$$

Lean4

@[gcongr]
theorem verts_mono {H H' : G.Subgraph} (h : H ≤ H') : H.verts ⊆ H'.verts :=
  h.1

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

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

Разделы

Аффилиация

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