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

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

@[simp]

theorem Finset.mem_powerset {α : Type u_1} {s : Finset α} {t : Finset α} : s ∈ Finset.powerset t ↔ s ⊆ t

@[simp]

theorem Finset.coe_powerset {α : Type u_1} (s : Finset α) : ↑(Finset.powerset s) = Finset.toSet ⁻¹' 𝒫↑s

theorem Finset.empty_mem_powerset {α : Type u_1} (s : Finset α) : ∅ ∈ Finset.powerset s

theorem Finset.mem_powerset_self {α : Type u_1} (s : Finset α) : s ∈ Finset.powerset s

theorem Finset.powerset_nonempty {α : Type u_1} (s : Finset α) : (Finset.powerset s).Nonempty

@[simp]

theorem Finset.powerset_mono {α : Type u_1} {s : Finset α} {t : Finset α} : Finset.powerset s ⊆ Finset.powerset t ↔ 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 α} : Finset.powerset s = Finset.powerset t ↔ s = t

@[simp]

theorem Finset.powerset_empty {α : Type u_1} : Finset.powerset ∅ = {∅}

@[simp]

theorem Finset.powerset_eq_singleton_empty {α : Type u_1} {s : Finset α} : Finset.powerset s = {∅} ↔ s = ∅

@[simp]

theorem Finset.card_powerset {α : Type u_1} (s : Finset α) : (Finset.powerset s).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 ∈ Finset.powerset s) (h : a ∉ s) : a ∉ t

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

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 ∈ Finset.powerset s), p t ⋯) ⋯

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 ∈ Finset.powerset s), p t ⋯) ⋯

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) ⋯

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

• Finset.ssubsets s = Finset.erase (Finset.powerset s) s

@[simp]

theorem Finset.mem_ssubsets {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : t ∈ Finset.ssubsets s ↔ t ⊂ s

theorem Finset.empty_mem_ssubsets {α : Type u_1} [DecidableEq α] {s : Finset α} (h : s.Nonempty) : ∅ ∈ Finset.ssubsets s

instance 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 ∈ Finset.ssubsets s), p t ⋯) ⋯

instance 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 ∈ Finset.ssubsets s), 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 : 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) : Finset.powersetCard n s ⊆ Finset.powersetCard n t

@[simp]

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

Formula for the Number of Combinations

@[simp]

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

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

@[simp]

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

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

@[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) (Finset.powerset s)

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

@[simp]

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

@[simp]

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

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

theorem Finset.powerset_card_disjiUnion {α : Type u_1} (s : Finset α) : Finset.powerset s = Finset.disjiUnion (Finset.range (s.card + 1)) (fun (i : ℕ) => Finset.powersetCard i s) ⋯

theorem Finset.powerset_card_biUnion {α : Type u_1} [DecidableEq (Finset α)] (s : Finset α) : Finset.powerset s = Finset.biUnion (Finset.range (s.card + 1)) fun (i : ℕ) => Finset.powersetCard i s

theorem Finset.powersetCard_sup {α : Type u_1} [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.card) : Finset.sup (Finset.powersetCard (Nat.succ n) u) id = u

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