card_interedges_add_card_interedges_compl

English

The sum of the cardinalities of interedges(r,s,t) and interedges(not r, s,t) equals |s|·|t|.

Русский

Сумма кардинальностей interedges(r,s,t) и interedges(not r, s,t) равна |s|·|t|.

LaTeX

$$$ |\mathrm{interedges}(r,s,t)| + |\mathrm{interedges}(\neg r,s,t)| = |s| \cdot |t| $$$

Lean4

theorem card_interedges_add_card_interedges_compl (s : Finset α) (t : Finset β) :
    #(interedges r s t) + #(interedges (fun x y ↦ ¬r x y) s t) = #s * #t := by
  classical
  rw [← card_product, interedges, interedges, ← card_union_of_disjoint, filter_union_filter_neg_eq]
  exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

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