Theorems · Theorem · combinatorics

Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow

∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β}
  [inst : (a : α) → (b : β) → Decidable (r a b)],
  ∑ a ∈ s, (Finset.bipartiteAbove r t a).card = ∑ b ∈ t, (Finset.bipartiteBelow r s b).card

Defined in

Mathlib.Combinatorics.Enumerative.DoubleCounting

Cited by

5 results in Mathlib

Foundations

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

Assumes

Decidable