Documentation

Mathlib.Data.Fintype.Powerset

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

instance Finset.fintype {α : Type u_1} [Fintype α] :
Equations
  • Finset.fintype = { elems := Finset.univ.powerset, complete := }
@[simp]
theorem Fintype.card_finset {α : Type u_1} [Fintype α] :
@[simp]
theorem Finset.powerset_univ {α : Type u_1} [Fintype α] :
Finset.univ.powerset = Finset.univ
theorem Finset.filter_subset_univ {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
Finset.filter (fun (t : Finset α) => t s) Finset.univ = s.powerset
@[simp]
theorem Finset.powerset_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} :
s.powerset = Finset.univ s = Finset.univ
theorem Finset.mem_powersetCard_univ {α : Type u_1} [Fintype α] {s : Finset α} {k : } :
s Finset.powersetCard k Finset.univ s.card = k
@[simp]
theorem Finset.univ_filter_card_eq (α : Type u_1) [Fintype α] (k : ) :
Finset.filter (fun (s : Finset α) => s.card = k) Finset.univ = Finset.powersetCard k Finset.univ
@[simp]
theorem Fintype.card_finset_len {α : Type u_1} [Fintype α] (k : ) :
Fintype.card { s : Finset α // s.card = k } = (Fintype.card α).choose k
instance Set.fintype {α : Type u_1} [Fintype α] :
Equations
  • Set.fintype = { elems := Finset.map Finset.coeEmb.toEmbedding Finset.univ, complete := }
instance Set.finite' {α : Type u_1} [Finite α] :
Finite (Set α)
Equations
  • =
@[simp]
theorem Fintype.card_set {α : Type u_1} [Fintype α] :