edgeSet_deleteEdges

Mathlib.Combinatorics.SimpleGraph.DeleteEdges

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

English

After deleting a finite set s of edges, the edgeFinset becomes the original edgeFinset minus s.

Русский

После удаления конечного множества рёбер s, edgeFinset графа становится edgeFinset графа минус s.

LaTeX

$$ (G.deleteEdges s).edgeFinset = G.edgeFinset \ s$$

Lean4

theorem edgeSet_deleteEdges (s : Set (Sym2 V)) : (G.deleteEdges s).edgeSet = G.edgeSet \ s := by simp [deleteEdges]

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

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

Разделы

Аффилиация

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