fintype instance for Set α, when α is a fintype

ink

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

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

ink

@[simp]

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