edgeSet_sdiff

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

The edge set of the set difference G1 \ G2 equals E(G1) \ E(G2).

Русский

Множество ребер графа \ G1 равно множеству ребер G1 \ G2.

LaTeX

$$$$ E(G_1 \ G_2) = E(G_1) \ E(G_2). $$$$

Lean4

@[simp]
theorem edgeSet_sdiff : (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet :=
  by
  ext ⟨x, y⟩
  rfl

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

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

Разделы

Аффилиация

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