deleteEdges_edgeSet

Mathlib.Combinatorics.SimpleGraph.DeleteEdges

URI: https://scilib.ai/kg/mathlib#SimpleGraph.deleteEdges_edgeSet

English

Removing the set of edges from G yields G with those edges removed from its edge set.

Русский

Удаление множества рёбер из G даёт граф G с удалёнными ребрами из этого множества.

LaTeX

$$G.deleteEdges s = G \ fromEdgeSet s$$

Lean4

@[simp]
theorem deleteEdges_edgeSet (G G' : SimpleGraph V) : G.deleteEdges G'.edgeSet = G \ G' := by ext; simp

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

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

Разделы

Аффилиация

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