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
@[simp]
theorem Finset.mem_powerset {α : Type u_1} {s t : Finset α} :
@[simp]
theorem Finset.coe_powerset {α : Type u_1} (s : Finset α) :
theorem Finset.mem_powerset_self {α : Type u_1} (s : Finset α) :
@[simp]
theorem Finset.powerset_mono {α : Type u_1} {s t : Finset α} :
@[simp]
theorem Finset.powerset_inj {α : Type u_1} {s t : Finset α} :
@[simp]
@[simp]
@[simp]
theorem Finset.card_powerset {α : Type u_1} (s : Finset α) :

Number of Subsets of a Set

theorem Finset.not_mem_of_mem_powerset_of_not_mem {α : Type u_1} {s t : Finset α} {a : α} (ht : t s.powerset) (h : as) :
at
theorem Finset.powerset_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
theorem Finset.pairwiseDisjoint_pair_insert {α : Type u_1} {s : Finset α} [DecidableEq α] {a : α} (ha : as) :
(↑s.powerset).PairwiseDisjoint fun (t : Finset α) => {t, insert a t}
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
@[simp]
theorem Finset.mem_ssubsets {α : Type u_1} [DecidableEq α] {s t : Finset α} :
theorem Finset.empty_mem_ssubsets {α : Type u_1} [DecidableEq α] {s : Finset α} (h : s.Nonempty) :
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 t : Finset α} :
s powersetCard n t s t s.card = n
@[simp]
theorem Finset.powersetCard_mono {α : Type u_1} {n : } {s t : Finset α} (h : s t) :
@[simp]
theorem Finset.card_powersetCard {α : Type u_1} (n : ) (s : Finset α) :

Formula for the Number of Combinations

@[simp]
theorem Finset.powersetCard_zero {α : Type u_1} (s : Finset α) :
theorem Finset.powersetCard_one {α : Type u_1} (s : Finset α) :
powersetCard 1 s = 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) :
theorem Finset.powersetCard_eq_filter {α : Type u_1} {n : } {s : Finset α} :
powersetCard n s = 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 α} :
theorem Finset.powersetCard_nonempty_of_le {α : Type u_1} {n : } {s : Finset α} :

Alias of the reverse direction of Finset.powersetCard_nonempty.

@[simp]
theorem Finset.powersetCard_self {α : Type u_1} (s : Finset α) :
theorem Finset.powerset_card_disjiUnion {α : Type u_1} (s : Finset α) :
s.powerset = (range (s.card + 1)).disjiUnion (fun (i : ) => powersetCard i s)
theorem Finset.powerset_card_biUnion {α : Type u_1} [DecidableEq (Finset α)] (s : Finset α) :
s.powerset = (range (s.card + 1)).biUnion fun (i : ) => powersetCard i s
theorem Finset.powersetCard_sup {α : Type u_1} [DecidableEq α] (u : Finset α) (n : ) (hn : n < u.card) :
theorem Finset.powersetCard_map {α : Type u_1} {β : Type u_2} (f : α β) (n : ) (s : Finset α) :