Counting Supersets of Two Fixed Subsets

This is a finite-set counting identity for two fixed subsets of equal size.

Let $\alpha$ be a type with decidable equality, let $U$ be a finite subset of $\alpha$, and let $d$ be a natural number. Assume:

1. $|U| = 3d$.
2. $F$ and $F'$ are $d$-element subsets of $U$.

Then the number of $2d$-element subsets $E$ of $U$ that contain $F \cup F'$ is

The statement provides a reusable combinatorial count for supersets of a union of two $d$-element subsets, parameterized by the size of their intersection.

Formalization Note The finite-set families are represented by Finset.powersetCard and filtered using Finset.filter; the binomial coefficient is Nat.choose.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Tensor. Shown in its original module context. Proof omitted.

theorem card_filter_union_subset (U : Finset α) {d : ℕ} (hU : U.card = 3 * d) {F F' : Finset α}
    (hF : F ∈ U.powersetCard d) (hF' : F' ∈ U.powersetCard d) :
    ((U.powersetCard (2 * d)).filter fun E => F ∪ F' ⊆ E).card =
      (d + (F ∩ F').card).choose d

Module navigation

Module: Analysis/Tensor/Symmetrization.

Next: sum_choose_mul_card_filter_subset.

Source excerpt, lines 64–67 · Frozen source 408915f.