# Documentation

Mathlib.Data.Finset.Powerset

# 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).

Instances For
@[simp]
theorem Finset.mem_powerset {α : Type u_1} {s : } {t : } :
s t
@[simp]
theorem Finset.coe_powerset {α : Type u_1} (s : ) :
↑() = Finset.toSet ⁻¹' 𝒫s
theorem Finset.empty_mem_powerset {α : Type u_1} (s : ) :
theorem Finset.mem_powerset_self {α : Type u_1} (s : ) :
theorem Finset.powerset_nonempty {α : Type u_1} (s : ) :
@[simp]
theorem Finset.powerset_mono {α : Type u_1} {s : } {t : } :
s t
theorem Finset.powerset_injective {α : Type u_1} :
Function.Injective Finset.powerset
@[simp]
theorem Finset.powerset_inj {α : Type u_1} {s : } {t : } :
s = t
@[simp]
theorem Finset.powerset_empty {α : Type u_1} :
@[simp]
theorem Finset.powerset_eq_singleton_empty {α : Type u_1} {s : } :
s =
@[simp]
theorem Finset.card_powerset {α : Type u_1} (s : ) :
= 2 ^

Number of Subsets of a Set

theorem Finset.not_mem_of_mem_powerset_of_not_mem {α : Type u_1} {s : } {t : } {a : α} (ht : ) (h : ¬a s) :
¬a t
theorem Finset.powerset_insert {α : Type u_1} [] (s : ) (a : α) :
instance Finset.decidableExistsOfDecidableSubsets {α : Type u_1} {s : } {p : (t : ) → t sProp} [(t : ) → (h : t s) → Decidable (p t h)] :
Decidable (t h, p t h)

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

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.

def Finset.decidableExistsOfDecidableSubsets' {α : Type u_1} {s : } {p : Prop} (hu : (t : ) → t sDecidable (p t)) :
Decidable (t _h, p t)

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

Instances For
def Finset.decidableForallOfDecidableSubsets' {α : Type u_1} {s : } {p : Prop} (hu : (t : ) → t sDecidable (p t)) :
Decidable ((t : ) → t sp t)

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

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

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

Instances For
@[simp]
theorem Finset.mem_ssubsets {α : Type u_1} [] {s : } {t : } :
t s
theorem Finset.empty_mem_ssubsets {α : Type u_1} [] {s : } (h : ) :
instance Finset.decidableExistsOfDecidableSSubsets {α : Type u_1} [] {s : } {p : (t : ) → t sProp} [(t : ) → (h : t s) → Decidable (p t h)] :
Decidable (t h, p t h)

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

instance 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.

def Finset.decidableExistsOfDecidableSSubsets' {α : Type u_1} [] {s : } {p : Prop} (hu : (t : ) → t sDecidable (p t)) :
Decidable (t _h, p t)

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

Instances For
def Finset.decidableForallOfDecidableSSubsets' {α : Type u_1} [] {s : } {p : Prop} (hu : (t : ) → t sDecidable (p t)) :
Decidable ((t : ) → t sp t)

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

Instances For
def Finset.powersetLen {α : Type u_1} (n : ) (s : ) :

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

Instances For
theorem Finset.mem_powersetLen {α : Type u_1} {n : } {s : } {t : } :
s s t = n

Formula for the Number of Combinations

@[simp]
theorem Finset.powersetLen_mono {α : Type u_1} {n : } {s : } {t : } (h : s t) :
@[simp]
theorem Finset.card_powersetLen {α : Type u_1} (n : ) (s : ) :
=

Formula for the Number of Combinations

@[simp]
theorem Finset.powersetLen_zero {α : Type u_1} (s : ) :
= {}
@[simp]
theorem Finset.powersetLen_empty {α : Type u_1} (n : ) {s : } (h : < n) :
theorem Finset.powersetLen_eq_filter {α : Type u_1} {n : } {s : } :
= Finset.filter (fun x => = n) ()
theorem Finset.powersetLen_succ_insert {α : Type u_1} [] {x : α} {s : } (h : ¬x s) (n : ) :
theorem Finset.powersetLen_nonempty {α : Type u_1} {n : } {s : } (h : n ) :
@[simp]
theorem Finset.powersetLen_self {α : Type u_1} (s : ) :
= {s}
theorem Finset.pairwise_disjoint_powersetLen {α : Type u_1} (s : ) :
Pairwise fun i j => Disjoint () ()
theorem Finset.powerset_card_disjiUnion {α : Type u_1} (s : ) :
= Finset.disjiUnion (Finset.range ( + 1)) (fun i => ) (_ : Set.Pairwise ↑(Finset.range ( + 1)) fun i j => Disjoint () ())
theorem Finset.powerset_card_biUnion {α : Type u_1} [] (s : ) :
= Finset.biUnion (Finset.range ( + 1)) fun i =>
theorem Finset.powersetLen_sup {α : Type u_1} [] (u : ) (n : ) (hn : n < ) :
Finset.sup () id = u
@[simp]
theorem Finset.powersetLen_card_add {α : Type u_1} (s : ) {i : } (hi : 0 < i) :
@[simp]
theorem Finset.map_val_val_powersetLen {α : Type u_1} (s : ) (i : ) :
Multiset.map Finset.val ().val = Multiset.powersetLen i s.val
theorem Finset.powersetLen_map {α : Type u_1} {β : Type u_2} (f : α β) (n : ) (s : ) :
Finset.powersetLen n () = Finset.map ().toEmbedding ()