The powerset of a finset

powerset

def Finset.powerset {α : Type u_1} (s : Finset α) : Finset (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 t : Finset α} : s ∈ t.powerset ↔ s ⊆ t

@[simp]

theorem Finset.coe_powerset {α : Type u_1} (s : Finset α) : ↑s.powerset = SetLike.coe ⁻¹' 𝒫 ↑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 t : Finset α} : s.powerset ⊆ t.powerset ↔ s ⊆ t

theorem Finset.powerset_injective {α : Type u_1} : Function.Injective powerset

@[simp]

theorem Finset.powerset_inj {α : Type u_1} {s 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 = ∅

theorem Finset.image_injOn_powerset_of_injOn {α : Type u_1} {s : Finset α} {β : Type u_2} [DecidableEq β] {f : α → β} (H : Set.InjOn f ↑s) : Set.InjOn (fun (x : Finset α) => image f x) ↑s.powerset

theorem Finset.injOn_image_of_biUnion_injOn {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {S : Finset (Finset α)} {f : α → β} (hf : Set.InjOn f ↑(S.biUnion id)) : Set.InjOn (fun (x : Finset α) => image f x) ↑S

Variant of Finset.image_injOn_powerset_of_injOn for a family S of finsets whose union supports an InjOn hypothesis, rather than the full powerset of a set.

theorem Finset.biUnion_id_subset_iff_subset_powerset {α : Type u_1} {t : Finset α} [DecidableEq α] {s : Finset (Finset α)} : s.biUnion id ⊆ t ↔ s ⊆ t.powerset

s.biUnion id ⊆ t iff every member of s is a subset of t, i.e. s ⊆ t.powerset.

theorem Finset.image_surjOn_powerset {α : Type u_1} {s : Finset α} {β : Type u_2} [DecidableEq β] {f : α → β} : Set.SurjOn (fun (x : Finset α) => image f x) ↑s.powerset ↑(image f s).powerset

theorem Finset.powerset_image {α : Type u_1} {s : Finset α} {β : Type u_2} [DecidableEq β] {f : α → β} : (image f s).powerset = image (fun (x : Finset α) => image f x) s.powerset

@[simp]

theorem Finset.card_powerset {α : Type u_1} (s : Finset α) : s.powerset.card = 2 ^ s.card

Number of Subsets of a Set

theorem Finset.notMem_of_mem_powerset_of_notMem {α : Type u_1} {s t : Finset α} {a : α} (ht : t ∈ s.powerset) (h : a ∉ s) : a ∉ t

theorem Finset.powerset_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : (insert a s).powerset = s.powerset ∪ image (insert a) s.powerset

theorem Finset.pairwiseDisjoint_pair_insert {α : Type u_1} {s : Finset α} [DecidableEq α] {a : α} (ha : a ∉ s) : (↑s.powerset).PairwiseDisjoint fun (t : Finset α) => {t, insert a t}

@[implicit_reducible]

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

• Finset.decidableExistsOfDecidableSubsets = decidable_of_iff (∃ (t : Finset α) (hs : t ∈ s.powerset), p t ⋯) ⋯

@[implicit_reducible]

instance Finset.decidableForallOfDecidableSubsets {α : Type u_1} {s : Finset α} {p : (t : Finset α) → t ⊆ s → Prop} [(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

• Finset.decidableForallOfDecidableSubsets = decidable_of_iff (∀ (t : Finset α) (h : t ∈ s.powerset), p t ⋯) ⋯

@[implicit_reducible]

instance Finset.decidableExistsOfDecidableSubsets' {α : Type u_1} {s : Finset α} {p : Finset α → Prop} [(t : Finset α) → Decidable (p t)] : Decidable (∃ t ⊆ s, p t)

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

Equations

• Finset.decidableExistsOfDecidableSubsets' = decidable_of_iff (∃ (t : Finset α) (_ : t ⊆ s), p t) ⋯

@[implicit_reducible]

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

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

Equations

• Finset.decidableForallOfDecidableSubsets' = decidable_of_iff (∀ t ⊆ s, p t) ⋯

def Finset.ssubsets {α : Type u_1} [DecidableEq α] (s : Finset α) : Finset (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 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 ⊂ s → Prop} [(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

• Finset.decidableExistsOfDecidableSSubsets = decidable_of_iff (∃ (t : Finset α) (hs : t ∈ s.ssubsets), p t ⋯) ⋯

def Finset.decidableForallOfDecidableSSubsets {α : Type u_1} [DecidableEq α] {s : Finset α} {p : (t : Finset α) → t ⊂ s → Prop} [(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

• Finset.decidableForallOfDecidableSSubsets = decidable_of_iff (∀ (t : Finset α) (h : t ∈ s.ssubsets), p t ⋯) ⋯

def Finset.decidableExistsOfDecidableSSubsets' {α : Type u_1} [DecidableEq α] {s : Finset α} {p : Finset α → Prop} (hu : (t : Finset α) → t ⊂ s → Decidable (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

• Finset.decidableExistsOfDecidableSSubsets' hu = Finset.decidableExistsOfDecidableSSubsets

def Finset.decidableForallOfDecidableSSubsets' {α : Type u_1} [DecidableEq α] {s : Finset α} {p : Finset α → Prop} (hu : (t : Finset α) → t ⊂ s → Decidable (p t)) : Decidable (∀ t ⊂ s, 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' hu = Finset.decidableForallOfDecidableSSubsets

def Finset.powersetCard {α : Type u_1} (n : ℕ) (s : Finset α) : Finset (Finset α)

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

Equations

• Finset.powersetCard n s = { val := Multiset.pmap Finset.mk (Multiset.powersetCard n s.val) ⋯, nodup := ⋯ }

@[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) : powersetCard n s ⊆ powersetCard n t

@[simp]

theorem Finset.card_powersetCard {α : Type u_1} (n : ℕ) (s : Finset α) : (powersetCard n s).card = s.card.choose n

Formula for the Number of Combinations

theorem Finset.filter_powersetCard_subset {α : Type u_1} [DecidableEq α] (s t : Finset α) (n : ℕ) (hst : s ⊆ t) (hsn : s.card ≤ n) : {x ∈ powersetCard n t | s ⊆ x} = image (fun (x : Finset α) => x ∪ s) (powersetCard (n - s.card) (t \ s))

The n-element subsets of t containing s are exactly the (n - s.card)-element subsets of t \ s, unioned with s.

theorem Finset.card_filter_powersetCard_subset {α : Type u_1} [DecidableEq α] (s t : Finset α) (n : ℕ) (hst : s ⊆ t) (hsn : s.card ≤ n) : {x ∈ powersetCard n t | s ⊆ x}.card = (t.card - s.card).choose (n - s.card)

The number of n-element subsets of t containing s equals Nat.choose (#t - #s) (n - #s).

@[simp]

theorem Finset.powersetCard_zero {α : Type u_1} (s : Finset α) : powersetCard 0 s = {∅}

theorem Finset.powersetCard_empty_subsingleton {α : Type u_1} (n : ℕ) : (↑(powersetCard n ∅)).Subsingleton

@[simp]

theorem Finset.map_val_val_powersetCard {α : Type u_1} (s : Finset α) (i : ℕ) : Multiset.map val (powersetCard i s).val = Multiset.powersetCard i s.val

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 α} : powersetCard n s = ∅ ↔ s.card < n

@[simp]

theorem Finset.powersetCard_card_add {α : Type u_1} {n : ℕ} (s : Finset α) (hn : 0 < n) : powersetCard (s.card + n) s = ∅

theorem Finset.powersetCard_eq_filter {α : Type u_1} {n : ℕ} {s : Finset α} : powersetCard n s = {x ∈ s.powerset | x.card = n}

theorem Finset.powersetCard_succ_insert {α : Type u_1} [DecidableEq α] {x : α} {s : Finset α} (h : x ∉ s) (n : ℕ) : powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

@[simp]

theorem Finset.powersetCard_nonempty {α : Type u_1} {n : ℕ} {s : Finset α} : (powersetCard n s).Nonempty ↔ n ≤ s.card

theorem Finset.powersetCard_nonempty_of_le {α : Type u_1} {n : ℕ} {s : Finset α} : n ≤ s.card → (powersetCard n s).Nonempty

Alias of the reverse direction of Finset.powersetCard_nonempty.

@[simp]

theorem Finset.powersetCard_self {α : Type u_1} (s : Finset α) : powersetCard s.card s = {s}

theorem Finset.pairwise_disjoint_powersetCard {α : Type u_1} (s : Finset α) : Pairwise fun (i j : ℕ) => Disjoint (powersetCard i s) (powersetCard j s)

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) : (powersetCard n.succ u).sup id = u

theorem Finset.powersetCard_biUnion {α : Type u_1} {s : Finset α} [DecidableEq α] {r : ℕ} (hr : r ≠ 0) (hrs : r ≤ s.card) : (powersetCard r s).biUnion id = s

The union of all r-element subsets of s is s, provided 1 ≤ r ≤ #s.

theorem Finset.eq_of_powersetCard_eq {α : Type u_1} {a b : Finset α} {r : ℕ} (hab : a.card = b.card) (hr₀ : r ≠ 0) (hra : r ≤ a.card) (h : powersetCard r a = powersetCard r b) : a = b

If two finsets of equal cardinality have the same r-element subsets for some 1 ≤ r ≤ #a, they are equal.

theorem Finset.powersetCard_injOn {α : Type u_1} {q r : ℕ} (hr₀ : r ≠ 0) (hrq : r ≤ q) : Set.InjOn (fun (a : Finset α) => powersetCard r a) {a : Finset α | a.card = q}

For 1 ≤ r ≤ q, the map powersetCard r is injective on the finsets of cardinality q.

theorem Finset.powersetCard_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (n : ℕ) (s : Finset α) : powersetCard n (map f s) = map (mapEmbedding f).toEmbedding (powersetCard n s)