fintype instance for Set α, when α is a fintype

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

Equations

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

@[simp]

theorem Fintype.card_finset {α : Type u_1} [Fintype α] : card (Finset α) = 2 ^ card α

@[simp]

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

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

@[simp]

theorem Finset.powerset_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} : s.powerset = univ ↔ s = univ

theorem Finset.mem_powersetCard_univ {α : Type u_1} [Fintype α] {s : Finset α} {k : ℕ} : s ∈ powersetCard k univ ↔ s.card = k

@[simp]

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

@[simp]

theorem Fintype.card_finset_len {α : Type u_1} [Fintype α] (k : ℕ) : card { s : Finset α // s.card = k } = (card α).choose k

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

Equations

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

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

@[simp]

theorem Fintype.card_set {α : Type u_1} [Fintype α] : card (Set α) = 2 ^ card α