English
The intersection of the complements of neighbor sets, with or without removing v and w, matches the symmetric difference description that aligns with the complement of their unions.
Русский
Пересечение дополнений множеств соседей, возможно с удалением v и w, совпадает с описанием через дополнение к их объединению.
LaTeX
$$Eq (Finset.instInter.inter (Finset.instSDiff.sdiff (Finset.booleanAlgebra.compl (G.neighborFinset v)) (Finset.instSingleton.singleton v)) (Finset.instSDiff.sdiff (Finset.booleanAlgebra.compl (G.neighborFinset w)) (Finset.instSingleton.singleton w))) (Finset.instSDiff.sdiff (Finset.instInter.inter (Finset.booleanAlgebra.compl (G.neighborFinset v)) (Finset.booleanAlgebra.compl (G.neighborFinset w))) (Finset.instUnion.union (Finset.instSingleton.singleton w) (Finset.instSingleton.singleton v)))$$
Lean4
theorem compl_neighborFinset_sdiff_inter_eq {v w : V} :
(G.neighborFinset v)ᶜ \ { v } ∩ ((G.neighborFinset w)ᶜ \ { w }) =
((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({ w } ∪ { v }) :=
by grind
