deleteEdges_le

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

Deleting edges is a subgraph containment operation: G'.deleteEdges s ≤ G'.

Русский

Удаление рёбер является операцией вложенности подграфа: G'.deleteEdges s ≤ G'.

LaTeX

$$$ G'.deleteEdges s \\le G' $$$

Lean4

theorem deleteEdges_le : G'.deleteEdges s ≤ G' := by constructor <;> simp +contextual

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

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

Разделы

Аффилиация

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