English
Again, a formal identity expressing the equality of the two ways of forming the intersection and complement of neighbor sets.
Русский
Ещё одно формальное тождество для пересечения дополнений множеств соседей.
LaTeX
$$Eq (Finset.instInter.inter (Finset.booleanAlgebra.compl (G.neighborFinset v)) (Finset.booleanAlgebra.compl (G.neighborFinset w))) (Finset.instInter.inter (Finset.booleanAlgebra.compl (G.neighborFinset v)) (Finset.booleanAlgebra.compl (G.neighborFinset w)))$$
Lean4
theorem sdiff_compl_neighborFinset_inter_eq {v w : V} (h : G.Adj v w) :
((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({ w } ∪ { v }) = (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ :=
by
ext
simp only [and_imp, mem_union, mem_sdiff, mem_compl, and_iff_left_iff_imp, mem_neighborFinset, mem_inter,
mem_singleton]
rintro hnv hnw (rfl | rfl)
· exact hnv h
· apply hnw
rwa [adj_comm]