compl_neighborSet_disjoint — Mathlib

English

The neighbor set of v and the complement neighborhood set of v are disjoint.

Русский

Множество соседей вершины v и множество её несовседников по отношению к комплементу не пересекаются.

LaTeX

$$$\\operatorname{Disjoint}(G.neighborSet(v), G^{c}.neighborSet(v))$$$

Lean4

theorem compl_neighborSet_disjoint (G : SimpleGraph V) (v : V) : Disjoint (G.neighborSet v) (Gᶜ.neighborSet v) :=
  by
  rw [Set.disjoint_iff]
  rintro w ⟨h, h'⟩
  rw [mem_neighborSet, compl_adj] at h'
  exact h'.2 h

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