neighborSet_compl — Mathlib

English

The complement of the neighbor set equals the complement minus the vertex itself.

Русский

Комплемент множества соседей вершины равен комплементу множества соседей без самой вершины.

LaTeX

$$$G^{c}.neighborSet(v) = (G.neighborSet(v))^{c} \\ \\{ v \\}$$$

Lean4

theorem neighborSet_compl (G : SimpleGraph V) (v : V) : Gᶜ.neighborSet v = (G.neighborSet v)ᶜ \ { v } :=
  by
  ext w
  simp [and_comm, eq_comm]

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