Documentation

Mathlib.Data.Fintype.Powerset

fintype instance for Set α, when α is a fintype #

source
instance Finset.fintype {α : Type u_1} [Fintype α] :
Fintype (Finset α)
source
@[simp]
theorem Fintype.card_finset {α : Type u_1} [Fintype α] :
Fintype.card (Finset α) = 2 ^ Fintype.card α
source
@[simp]
theorem Finset.powerset_univ {α : Type u_1} [Fintype α] :
Finset.powerset Finset.univ = Finset.univ
source
@[simp]
theorem Finset.powerset_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} :
Finset.powerset s = Finset.univ ↔ s = Finset.univ
source
@[simp]
theorem Finset.mem_powerset_len_univ_iff {α : Type u_1} [Fintype α] {s : Finset α} {k : ℕ} :
s ∈ Finset.powersetLen k Finset.univ ↔ Finset.card s = k
source
@[simp]
theorem Finset.univ_filter_card_eq (α : Type u_2) [Fintype α] (k : ℕ) :
Finset.filter (fun s => Finset.card s = k) Finset.univ = Finset.powersetLen k Finset.univ
source
@[simp]
theorem Fintype.card_finset_len {α : Type u_1} [Fintype α] (k : ℕ) :
Fintype.card { s // Finset.card s = k } = Nat.choose (Fintype.card α) k
source
instance Set.fintype {α : Type u_1} [Fintype α] :
Fintype (Set α)
source
instance Set.finite' {α : Type u_1} [Finite α] :
Finite (Set α)
source
@[simp]
theorem Fintype.card_set {α : Type u_1} [Fintype α] :
Fintype.card (Set α) = 2 ^ Fintype.card α