Equations
- Eq Finset.fintype { elems := Finset.univ.powerset, complete := ⋯ }
Instances For
theorem
Finset.mem_powersetCard_univ
{α : Type u_1}
[Fintype α]
{s : Finset α}
{k : Nat}
:
Iff (Membership.mem (powersetCard k univ) s) (Eq s.card k)
Equations
- Eq Set.fintype { elems := Finset.map Finset.coeEmb.toEmbedding Finset.univ, complete := ⋯ }