Documentation

Mathlib.Data.Fintype.Powerset

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

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