fintype instance for Set α, when α is a fintype

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

Equations

• Finset.fintype = { elems := Finset.powerset Finset.univ, complete := (_ : ∀ (x : Finset α), x ∈ Finset.powerset Finset.univ) }

@[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.powerset Finset.univ = Finset.univ

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• @Set.finite' = @Set.finite'.proof_1

@[simp]

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