mathlib3 documentation

data.fintype.powerset

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def finset.fintype {α : Type u_1} [fintype α] :
fintype (finset α)
Equations
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.univ.powerset = finset.univ
source
@[simp]
theorem finset.powerset_eq_univ {α : Type u_1} [fintype α] {s : finset α} :
s.powerset = finset.univ ↔ s = finset.univ
source
theorem finset.mem_powerset_len_univ_iff {α : Type u_1} [fintype α] {s : finset α} {k : ℕ} :
s ∈ finset.powerset_len k finset.univ ↔ s.card = k
source
@[simp]
theorem finset.univ_filter_card_eq (α : Type u_1) [fintype α] (k : ℕ) :
finset.filter (λ (s : finset α), s.card = k) finset.univ = finset.powerset_len k finset.univ
source
@[simp]
theorem fintype.card_finset_len {α : Type u_1} [fintype α] (k : ℕ) :
fintype.card {s // s.card = k} = (fintype.card α).choose k
source
@[protected, instance]
def set.fintype {α : Type u_1} [fintype α] :
fintype (set α)
Equations
source
@[protected, instance]
def set.finite' {α : Type u_1} [finite α] :
finite (set α)
source
@[simp]
theorem fintype.card_set {α : Type u_1} [fintype α] :
fintype.card (set α) = 2 ^ fintype.card α