Documentation

Mathlib.Data.Fintype.Powerset

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

source
instance Finset.fintype {α : Type u_1} [Fintype α] :
Fintype (Finset α)
Equations
    source
    @[simp]
    theorem Fintype.card_finset {α : Type u_1} [Fintype α] :
    card (Finset α) = 2 ^ card α
    source
    @[simp]
    theorem Finset.powerset_univ {α : Type u_1} [Fintype α] :
    univ.powerset = univ
    source
    theorem Finset.filter_subset_univ {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
    {t : Finset α | t ⊆ s} = s.powerset
    source
    @[simp]
    theorem Finset.powerset_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} :
    s.powerset = univ ↔ s = univ
    source
    theorem Finset.mem_powersetCard_univ {α : Type u_1} [Fintype α] {s : Finset α} {k : ℕ} :
    s ∈ powersetCard k univ ↔ s.card = k
    source
    @[simp]
    theorem Finset.univ_filter_card_eq (α : Type u_1) [Fintype α] (k : ℕ) :
    {s : Finset α | s.card = k} = powersetCard k univ
    source
    @[simp]
    theorem Fintype.card_finset_len {α : Type u_1} [Fintype α] (k : ℕ) :
    card { s : Finset α // s.card = k } = (card α).choose k
    source
    instance Set.fintype {α : Type u_1} [Fintype α] :
    Fintype (Set α)
    Equations
      source
      instance Set.instFinite {α : Type u_1} [Finite α] :
      Finite (Set α)
      source
      @[simp]
      theorem Fintype.card_set {α : Type u_1} [Fintype α] :
      card (Set α) = 2 ^ card α