Theorems · Theorem · combinatorics

Finset.filter_product_card

∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) (p : α → Prop) (q : β → Prop) [inst : DecidablePred p]
  [inst_1 : DecidablePred q],
  {x ∈ s ×ˢ t | p x.1 = q x.2}.card =
    (Finset.filter p s).card * (Finset.filter q t).card + {x ∈ s | ¬p x}.card * {x ∈ t | ¬q x}.card

Defined in

Mathlib.Data.Finset.Prod

Cited by

0 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidablePredDecidablePred