# The powerset of a finset #

### powerset #

def Finset.powerset {α : Type u_1} (s : ) :

When s is a finset, s.powerset is the finset of all subsets of s (seen as finsets).

Equations
• s.powerset = { val := Multiset.pmap Finset.mk s.val.powerset , nodup := }
Instances For
@[simp]
theorem Finset.mem_powerset {α : Type u_1} {s : } {t : } :
s t.powerset s t
@[simp]
theorem Finset.coe_powerset {α : Type u_1} (s : ) :
s.powerset = Finset.toSet ⁻¹' 𝒫s
theorem Finset.empty_mem_powerset {α : Type u_1} (s : ) :
s.powerset
theorem Finset.mem_powerset_self {α : Type u_1} (s : ) :
s s.powerset
theorem Finset.powerset_nonempty {α : Type u_1} (s : ) :
s.powerset.Nonempty
@[simp]
theorem Finset.powerset_mono {α : Type u_1} {s : } {t : } :
s.powerset t.powerset s t
theorem Finset.powerset_injective {α : Type u_1} :
Function.Injective Finset.powerset
@[simp]
theorem Finset.powerset_inj {α : Type u_1} {s : } {t : } :
s.powerset = t.powerset s = t
@[simp]
theorem Finset.powerset_empty {α : Type u_1} :
.powerset = {}
@[simp]
theorem Finset.powerset_eq_singleton_empty {α : Type u_1} {s : } :
s.powerset = {} s =
@[simp]
theorem Finset.card_powerset {α : Type u_1} (s : ) :
s.powerset.card = 2 ^ s.card

Number of Subsets of a Set

theorem Finset.not_mem_of_mem_powerset_of_not_mem {α : Type u_1} {s : } {t : } {a : α} (ht : t s.powerset) (h : as) :
at
theorem Finset.powerset_insert {α : Type u_1} [] (s : ) (a : α) :
(insert a s).powerset = s.powerset Finset.image (insert a) s.powerset
instance Finset.decidableExistsOfDecidableSubsets {α : Type u_1} {s : } {p : (t : ) → t sProp} [(t : ) → (h : t s) → Decidable (p t h)] :
Decidable (∃ (t : ) (h : t s), p t h)

For predicate p decidable on subsets, it is decidable whether p holds for any subset.

Equations
• Finset.decidableExistsOfDecidableSubsets = decidable_of_iff (∃ (t : ) (hs : t s.powerset), p t )
instance Finset.decidableForallOfDecidableSubsets {α : Type u_1} {s : } {p : (t : ) → t sProp} [(t : ) → (h : t s) → Decidable (p t h)] :
Decidable (∀ (t : ) (h : t s), p t h)

For predicate p decidable on subsets, it is decidable whether p holds for every subset.

Equations
• Finset.decidableForallOfDecidableSubsets = decidable_of_iff (∀ (t : ) (h : t s.powerset), p t )
instance Finset.decidableExistsOfDecidableSubsets' {α : Type u_1} {s : } {p : Prop} [(t : ) → Decidable (p t)] :
Decidable (∃ ts, p t)

For predicate p decidable on subsets, it is decidable whether p holds for any subset.

Equations
instance Finset.decidableForallOfDecidableSubsets' {α : Type u_1} {s : } {p : Prop} [(t : ) → Decidable (p t)] :
Decidable (∀ ts, p t)

For predicate p decidable on subsets, it is decidable whether p holds for every subset.

Equations
def Finset.ssubsets {α : Type u_1} [] (s : ) :

For s a finset, s.ssubsets is the finset comprising strict subsets of s.

Equations
• s.ssubsets = s.powerset.erase s
Instances For
@[simp]
theorem Finset.mem_ssubsets {α : Type u_1} [] {s : } {t : } :
t s.ssubsets t s
theorem Finset.empty_mem_ssubsets {α : Type u_1} [] {s : } (h : s.Nonempty) :
s.ssubsets
def Finset.decidableExistsOfDecidableSSubsets {α : Type u_1} [] {s : } {p : (t : ) → t sProp} [(t : ) → (h : t s) → Decidable (p t h)] :
Decidable (∃ (t : ) (h : t s), p t h)

For predicate p decidable on ssubsets, it is decidable whether p holds for any ssubset.

Equations
• Finset.decidableExistsOfDecidableSSubsets = decidable_of_iff (∃ (t : ) (hs : t s.ssubsets), p t )
Instances For
def Finset.decidableForallOfDecidableSSubsets {α : Type u_1} [] {s : } {p : (t : ) → t sProp} [(t : ) → (h : t s) → Decidable (p t h)] :
Decidable (∀ (t : ) (h : t s), p t h)

For predicate p decidable on ssubsets, it is decidable whether p holds for every ssubset.

Equations
• Finset.decidableForallOfDecidableSSubsets = decidable_of_iff (∀ (t : ) (h : t s.ssubsets), p t )
Instances For
def Finset.decidableExistsOfDecidableSSubsets' {α : Type u_1} [] {s : } {p : Prop} (hu : (t : ) → t sDecidable (p t)) :
Decidable (∃ (t : ) (_ : t s), p t)

A version of Finset.decidableExistsOfDecidableSSubsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

Equations
• = Finset.decidableExistsOfDecidableSSubsets
Instances For
def Finset.decidableForallOfDecidableSSubsets' {α : Type u_1} [] {s : } {p : Prop} (hu : (t : ) → t sDecidable (p t)) :
Decidable (∀ ts, p t)

A version of Finset.decidableForallOfDecidableSSubsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

Equations
• = Finset.decidableForallOfDecidableSSubsets
Instances For
def Finset.powersetCard {α : Type u_1} (n : ) (s : ) :

Given an integer n and a finset s, then powersetCard n s is the finset of subsets of s of cardinality n.

Equations
Instances For
@[simp]
theorem Finset.mem_powersetCard {α : Type u_1} {n : } {s : } {t : } :
s s t s.card = n
@[simp]
theorem Finset.powersetCard_mono {α : Type u_1} {n : } {s : } {t : } (h : s t) :
@[simp]
theorem Finset.card_powersetCard {α : Type u_1} (n : ) (s : ) :
.card = s.card.choose n

Formula for the Number of Combinations

@[simp]
theorem Finset.powersetCard_zero {α : Type u_1} (s : ) :
= {}
theorem Finset.powersetCard_empty_subsingleton {α : Type u_1} (n : ) :
(↑).Subsingleton
@[simp]
theorem Finset.map_val_val_powersetCard {α : Type u_1} (s : ) (i : ) :
Multiset.map Finset.val .val = Multiset.powersetCard i s.val
theorem Finset.powersetCard_one {α : Type u_1} (s : ) :
= Finset.map { toFun := singleton, inj' := } s
@[simp]
theorem Finset.powersetCard_eq_empty {α : Type u_1} {n : } {s : } :
s.card < n
@[simp]
theorem Finset.powersetCard_card_add {α : Type u_1} {n : } (s : ) (hn : 0 < n) :
Finset.powersetCard (s.card + n) s =
theorem Finset.powersetCard_eq_filter {α : Type u_1} {n : } {s : } :
= Finset.filter (fun (x : ) => x.card = n) s.powerset
theorem Finset.powersetCard_succ_insert {α : Type u_1} [] {x : α} {s : } (h : xs) (n : ) :
@[simp]
theorem Finset.powersetCard_nonempty {α : Type u_1} {n : } {s : } :
.Nonempty n s.card
@[simp]
theorem Finset.powersetCard_self {α : Type u_1} (s : ) :
Finset.powersetCard s.card s = {s}
theorem Finset.pairwise_disjoint_powersetCard {α : Type u_1} (s : ) :
Pairwise fun (i j : ) => Disjoint
theorem Finset.powerset_card_disjiUnion {α : Type u_1} (s : ) :
s.powerset = (Finset.range (s.card + 1)).disjiUnion (fun (i : ) => )
theorem Finset.powerset_card_biUnion {α : Type u_1} [] (s : ) :
s.powerset = (Finset.range (s.card + 1)).biUnion fun (i : ) =>
theorem Finset.powersetCard_sup {α : Type u_1} [] (u : ) (n : ) (hn : n < u.card) :
(Finset.powersetCard n.succ u).sup id = u
theorem Finset.powersetCard_map {α : Type u_1} {β : Type u_2} (f : α β) (n : ) (s : ) :
= Finset.map .toEmbedding