Documentation

Mathlib.Data.Finset.Powerset

The powerset of a finset #

powerset #

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

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 := }
@[simp]
theorem Finset.mem_powerset {α : Type u_1} {s : Finset α} {t : Finset α} :
s t.powerset s t
@[simp]
theorem Finset.coe_powerset {α : Type u_1} (s : Finset α) :
s.powerset = Finset.toSet ⁻¹' 𝒫s
theorem Finset.empty_mem_powerset {α : Type u_1} (s : Finset α) :
s.powerset
theorem Finset.mem_powerset_self {α : Type u_1} (s : Finset α) :
s s.powerset
theorem Finset.powerset_nonempty {α : Type u_1} (s : Finset α) :
s.powerset.Nonempty
@[simp]
theorem Finset.powerset_mono {α : Type u_1} {s : Finset α} {t : Finset α} :
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 : Finset α} {t : Finset α} :
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 : Finset α} :
s.powerset = {} s =
@[simp]
theorem Finset.card_powerset {α : Type u_1} (s : Finset α) :
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 : Finset α} {t : Finset α} {a : α} (ht : t s.powerset) (h : as) :
at
theorem Finset.powerset_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
(insert a s).powerset = s.powerset Finset.image (insert a) s.powerset
instance Finset.decidableExistsOfDecidableSubsets {α : Type u_1} {s : Finset α} {p : (t : Finset α) → t sProp} [(t : Finset α) → (h : t s) → Decidable (p t h)] :
Decidable (∃ (t : Finset α) (h : t s), p t h)

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

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

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

Equations
instance Finset.decidableExistsOfDecidableSubsets' {α : Type u_1} {s : Finset α} {p : Finset αProp} [(t : Finset α) → 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 : Finset α} {p : Finset αProp} [(t : Finset α) → 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} [DecidableEq α] (s : Finset α) :

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

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

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

Equations
def Finset.decidableForallOfDecidableSSubsets {α : Type u_1} [DecidableEq α] {s : Finset α} {p : (t : Finset α) → t sProp} [(t : Finset α) → (h : t s) → Decidable (p t h)] :
Decidable (∀ (t : Finset α) (h : t s), p t h)

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

Equations
def Finset.decidableExistsOfDecidableSSubsets' {α : Type u_1} [DecidableEq α] {s : Finset α} {p : Finset αProp} (hu : (t : Finset α) → t sDecidable (p t)) :
Decidable (∃ (t : Finset α) (_ : 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
def Finset.decidableForallOfDecidableSSubsets' {α : Type u_1} [DecidableEq α] {s : Finset α} {p : Finset αProp} (hu : (t : Finset α) → 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
def Finset.powersetCard {α : Type u_1} (n : ) (s : Finset α) :

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

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

Formula for the Number of Combinations

@[simp]
theorem Finset.powersetCard_zero {α : Type u_1} (s : Finset α) :
theorem Finset.powersetCard_empty_subsingleton {α : Type u_1} (n : ) :
(↑(Finset.powersetCard n )).Subsingleton
@[simp]
theorem Finset.map_val_val_powersetCard {α : Type u_1} (s : Finset α) (i : ) :
theorem Finset.powersetCard_one {α : Type u_1} (s : Finset α) :
Finset.powersetCard 1 s = Finset.map { toFun := singleton, inj' := } s
@[simp]
theorem Finset.powersetCard_eq_empty {α : Type u_1} {n : } {s : Finset α} :
@[simp]
theorem Finset.powersetCard_card_add {α : Type u_1} {n : } (s : Finset α) (hn : 0 < n) :
Finset.powersetCard (s.card + n) s =
theorem Finset.powersetCard_eq_filter {α : Type u_1} {n : } {s : Finset α} :
Finset.powersetCard n s = Finset.filter (fun (x : Finset α) => x.card = n) s.powerset
theorem Finset.powersetCard_succ_insert {α : Type u_1} [DecidableEq α] {x : α} {s : Finset α} (h : xs) (n : ) :
@[simp]
theorem Finset.powersetCard_nonempty {α : Type u_1} {n : } {s : Finset α} :
(Finset.powersetCard n s).Nonempty n s.card
theorem Finset.powersetCard_nonempty_of_le {α : Type u_1} {n : } {s : Finset α} :
n s.card(Finset.powersetCard n s).Nonempty

Alias of the reverse direction of Finset.powersetCard_nonempty.

@[simp]
theorem Finset.powersetCard_self {α : Type u_1} (s : Finset α) :
Finset.powersetCard s.card s = {s}
theorem Finset.powerset_card_disjiUnion {α : Type u_1} (s : Finset α) :
s.powerset = (Finset.range (s.card + 1)).disjiUnion (fun (i : ) => Finset.powersetCard i s)
theorem Finset.powerset_card_biUnion {α : Type u_1} [DecidableEq (Finset α)] (s : Finset α) :
s.powerset = (Finset.range (s.card + 1)).biUnion fun (i : ) => Finset.powersetCard i s
theorem Finset.powersetCard_sup {α : Type u_1} [DecidableEq α] (u : Finset α) (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 α) :