fintype instance for Set α, when α is a fintype

def Finset.fintype {α : Type u_1} [Fintype α] : Fintype (Finset α)

Equations

• Eq Finset.fintype { elems := Finset.univ.powerset, complete := ⋯ }

theorem Fintype.card_finset {α : Type u_1} [Fintype α] : Eq (card (Finset α)) (HPow.hPow 2 (card α))

theorem Finset.powerset_univ {α : Type u_1} [Fintype α] : Eq univ.powerset univ

theorem Finset.filter_subset_univ {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : Eq (filter (fun (t : Finset α) => HasSubset.Subset t s) univ) s.powerset

theorem Finset.powerset_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} : Iff (Eq s.powerset univ) (Eq s univ)

theorem Finset.mem_powersetCard_univ {α : Type u_1} [Fintype α] {s : Finset α} {k : Nat} : Iff (Membership.mem (powersetCard k univ) s) (Eq s.card k)

theorem Finset.univ_filter_card_eq (α : Type u_1) [Fintype α] (k : Nat) : Eq (filter (fun (s : Finset α) => Eq s.card k) univ) (powersetCard k univ)

theorem Fintype.card_finset_len {α : Type u_1} [Fintype α] (k : Nat) : Eq (card (Subtype fun (s : Finset α) => Eq s.card k)) ((card α).choose k)

def Set.fintype {α : Type u_1} [Fintype α] : Fintype (Set α)

Equations

• Eq Set.fintype { elems := Finset.map Finset.coeEmb.toEmbedding Finset.univ, complete := ⋯ }

theorem Set.instFinite {α : Type u_1} [Finite α] : Finite (Set α)

theorem Fintype.card_set {α : Type u_1} [Fintype α] : Eq (card (Set α)) (HPow.hPow 2 (card α))