sdiff_compl_neighborFinset_inter_eq

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]

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