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 α] : Fintype.card (Finset α) = 2 ^ Fintype.card α

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

Equations

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

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

@[simp]

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