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 α] :
@[simp]
theorem Finset.powerset_univ {α : Type u_1} [Fintype α] :
Finset.powerset Finset.univ = Finset.univ
theorem Finset.filter_subset_univ {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) :
Finset.filter (fun (t : Finset α) => t s) Finset.univ = Finset.powerset s
@[simp]
theorem Finset.powerset_eq_univ {α : Type u_1} [Fintype α] {s : Finset α} :
Finset.powerset s = 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 } = Nat.choose (Fintype.card α) k
instance Set.fintype {α : Type u_1} [Fintype α] :
Equations
instance Set.finite' {α : Type u_1} [Finite α] :
Finite (Set α)
Equations
  • =
@[simp]
theorem Fintype.card_set {α : Type u_1} [Fintype α] :