sdiff_edge

Mathlib.Combinatorics.SimpleGraph.Operations

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

English

If u and v are not adjacent in G, then removing the edge uv from G leaves G unchanged.

Русский

Если узлы u и v не смежны в G, то удаление ребра uv не меняет граф.

LaTeX

$$$\\neg G.Adj\\ u\\ v \\Rightarrow G \\\\ edge\\ u\\ v = G$$$

Lean4

theorem sdiff_edge {u v : V} (h : ¬G.Adj u v) : G \ edge u v = G := by simp [disjoint_edge, h]

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

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

Разделы

Аффилиация

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