deleteVerts_le

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

Deleting vertices is monotone with respect to subgraph inclusion: G'.deleteVerts s ≤ G'.

Русский

Удаление вершин монотонно по отношению к включению подграфов: G'.deleteVerts s ≤ G'.

LaTeX

$$$ G'.deleteVerts s \le G' $$$

Lean4

theorem deleteVerts_le : G'.deleteVerts s ≤ G' := by constructor <;> simp [Set.diff_subset]

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

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

Разделы

Аффилиация

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