card_interedges_add_card_interedges_compl

English

If s and t are disjoint, the number of interedges between s and t plus the number of non-edges equals the total number of pairs |s| · |t|.

Русский

Если s и t несовпадают, число межрёбер между s и t плюс число не-ребёр между s и t равно общему количеству пар |s||t|.

LaTeX

$$Disjoint s t → #(G.interedges s t) + #(Gᶜ.interedges s t) = #s * #t$$

Lean4

theorem card_interedges_add_card_interedges_compl (h : Disjoint s t) :
    #(G.interedges s t) + #(Gᶜ.interedges s t) = #s * #t :=
  by
  rw [← card_product, interedges_def, interedges_def]
  have : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬G.Adj e.1 e.2} :=
    by
    refine filter_congr fun x hx ↦ ?_
    rw [mem_product] at hx
    rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
  rw [this, ← card_union_of_disjoint, filter_union_filter_neg_eq]
  exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

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