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

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

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

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

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

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

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

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.

@[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 : Finset.Nonempty s) : ∅ ∈ 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 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} [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.

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

def Finset.decidableForallOfDecidableSSubsets' {α : 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.decidableForallOfDecidableSSubsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

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

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

theorem Finset.mem_powersetLen {α : Type u_1} {n : ℕ} {s : Finset α} {t : Finset α} : s ∈ Finset.powersetLen n t ↔ s ⊆ t ∧ Finset.card s = n

Formula for the Number of Combinations

@[simp]

theorem Finset.powersetLen_mono {α : Type u_1} {n : ℕ} {s : Finset α} {t : Finset α} (h : s ⊆ t) : Finset.powersetLen n s ⊆ Finset.powersetLen n t

@[simp]

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

Formula for the Number of Combinations

@[simp]

theorem Finset.powersetLen_zero {α : Type u_1} (s : Finset α) : Finset.powersetLen 0 s = {∅}

@[simp]

theorem Finset.powersetLen_empty {α : Type u_1} (n : ℕ) {s : Finset α} (h : Finset.card s < n) : Finset.powersetLen n s = ∅

theorem Finset.powersetLen_eq_filter {α : Type u_1} {n : ℕ} {s : Finset α} : Finset.powersetLen n s = Finset.filter (fun x => Finset.card x = n) (Finset.powerset s)

theorem Finset.powersetLen_succ_insert {α : Type u_1} [DecidableEq α] {x : α} {s : Finset α} (h : ¬x ∈ s) (n : ℕ) : Finset.powersetLen (Nat.succ n) (insert x s) = Finset.powersetLen (Nat.succ n) s ∪ Finset.image (insert x) (Finset.powersetLen n s)

theorem Finset.powersetLen_nonempty {α : Type u_1} {n : ℕ} {s : Finset α} (h : n ≤ Finset.card s) : Finset.Nonempty (Finset.powersetLen n s)

@[simp]

theorem Finset.powersetLen_self {α : Type u_1} (s : Finset α) : Finset.powersetLen (Finset.card s) s = {s}

theorem Finset.pairwise_disjoint_powersetLen {α : Type u_1} (s : Finset α) : Pairwise fun i j => Disjoint (Finset.powersetLen i s) (Finset.powersetLen j s)

theorem Finset.powerset_card_disjiUnion {α : Type u_1} (s : Finset α) : Finset.powerset s = Finset.disjiUnion (Finset.range (Finset.card s + 1)) (fun i => Finset.powersetLen i s) (_ : Set.Pairwise ↑(Finset.range (Finset.card s + 1)) fun i j => Disjoint (Finset.powersetLen i s) (Finset.powersetLen j s))

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

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

@[simp]

theorem Finset.powersetLen_card_add {α : Type u_1} (s : Finset α) {i : ℕ} (hi : 0 < i) : Finset.powersetLen (Finset.card s + i) s = ∅

@[simp]

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

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