English
Let s,t be Finsets and p on α, q on β. The cardinality of the filtered product equals the sum of two product terms: card(((s × t).filter (λ x: (p x.1) = (q x.2))).card = card(s.filter p) · card(t.filter q) + card(s.filter (¬p ·)) · card(t.filter (¬q ·)).
Русский
Пусть s,t — конечные множества, p — предикат на α, q — предикат на β. Кардинальность отфильтрованного произведения равна сумме двух произведений:
LaTeX
$$$\\operatorname{card}(((s \\\\times t).filter (\\\\lambda x: (p x.1) = (q x.2)))) = \\operatorname{card}(s.\\\\text{filter} p) \\\\cdot \\operatorname{card}(t.\\\\text{filter} q) + \\operatorname{card}(s.\\\\text{filter} (\\\\lnot p \\\\cdot)) \\\\cdot \\operatorname{card}(t.\\\\text{filter} (\\\\lnot q \\\\cdot))$$$
Lean4
theorem filter_product_card (s : Finset α) (t : Finset β) (p : α → Prop) (q : β → Prop) [DecidablePred p]
[DecidablePred q] :
((s ×ˢ t).filter fun x : α × β => (p x.1) = (q x.2)).card =
(s.filter p).card * (t.filter q).card + (s.filter (¬p ·)).card * (t.filter (¬q ·)).card :=
by
classical
rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
· apply congr_arg
ext ⟨a, b⟩
simp only [filter_union_right, mem_filter, mem_product]
constructor <;> intro h <;> use h.1
· simp only [h.2, Decidable.em, and_self]
· revert h
simp only [and_imp]
rintro _ _ (_ | _) <;> simp [*]
· apply Finset.disjoint_filter_filter'
exact (disjoint_compl_right.inf_left _).inf_right _
