theorem Finset.powersetCard_inter {α : Type u_1} [DecidableEq α] {s t : Finset α} {n : ℕ} : powersetCard n (s ∩ t) = powersetCard n s ∩ powersetCard n t

@[simp]

theorem Finset.disjoint_powersetCard_powersetCard {α : Type u_1} [DecidableEq α] {s t : Finset α} {n : ℕ} : Disjoint (powersetCard n s) (powersetCard n t) ↔ (s ∩ t).card < n