Theorem Definition:

        theorem Finset.mem_powersetCard {α : Type u_1}  {n : ℕ}  {s t : Finset α} : s ∈ powersetCard n t ↔ s ⊆ t ∧ s.card = n :=