neighborFinset_compl — Mathlib

English

In the complement graph, the neighbor Finset of v consists of vertices not adjacent to v, excluding v itself.

Русский

В дополнении графа множество соседей вершины v состоит из вершин, не смежных с v, исключая саму v.

LaTeX

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

Lean4

theorem neighborFinset_compl [DecidableEq V] [DecidableRel G.Adj] (v : V) :
    Gᶜ.neighborFinset v = (G.neighborFinset v)ᶜ \ { v } := by
  simp only [neighborFinset, neighborSet_compl, Set.toFinset_diff, Set.toFinset_compl, Set.toFinset_singleton]

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