neighborSet_union_compl_neighborSet_eq

English

The union of the neighbor set of v and the complement neighbor set of v equals the complement of {v}.

Русский

Объединение множества соседей v и множества несовседников v равно комплементу от {v}.

LaTeX

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

Lean4

theorem neighborSet_union_compl_neighborSet_eq (G : SimpleGraph V) (v : V) :
    G.neighborSet v ∪ Gᶜ.neighborSet v = { v }ᶜ := by
  ext w
  have h := @ne_of_adj _ G
  simp_rw [Set.mem_union, mem_neighborSet, compl_adj, Set.mem_compl_iff, Set.mem_singleton_iff]
  tauto

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