The powerset of a finset

powerset

ink

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

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

theorem Finset.powerset_inj {α : Type u_1} {s : Finset α} {t : Finset α} : Finset.powerset s = Finset.powerset t ↔ s = t

ink

@[simp]

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

ink

@[simp]

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

ink

@[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

ink

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

ink

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

ink

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

Equations

• Finset.decidableExistsOfDecidableSubsets = decidable_of_iff (∃ t hs, p t (_ : t ⊆ s)) (_ : (∃ t hs, p t (_ : t ⊆ s)) ↔ ∃ t h, p t h)

ink

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

• One or more equations did not get rendered due to their size.

ink

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.

Equations

• Finset.decidableExistsOfDecidableSubsets' hu = Finset.decidableExistsOfDecidableSubsets

ink

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.

Equations

• Finset.decidableForallOfDecidableSubsets' hu = Finset.decidableForallOfDecidableSubsets

ink

def Finset.ssubsets {α : Type u_1} [inst : 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

ink

@[simp]

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

ink

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

ink

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

Equations

• Finset.decidableExistsOfDecidableSsubsets = decidable_of_iff (∃ t hs, p t (_ : t ⊂ s)) (_ : (∃ t hs, p t (_ : t ⊂ s)) ↔ ∃ t h, p t h)

ink

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

• One or more equations did not get rendered due to their size.

ink

def Finset.decidableExistsOfDecidableSsubsets' {α : Type u_1} [inst : 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.

Equations

• Finset.decidableExistsOfDecidableSsubsets' hu = Finset.decidableExistsOfDecidableSsubsets

ink

def Finset.decidableForallOfDecidableSsubsets' {α : Type u_1} [inst : 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.

Equations

• Finset.decidableForallOfDecidableSsubsets' hu = Finset.decidableForallOfDecidableSsubsets

ink

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.

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

@[simp]

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

ink

@[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

ink

@[simp]

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

ink

@[simp]

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

ink

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)

ink

theorem Finset.powersetLen_succ_insert {α : Type u_1} [inst : 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)

ink

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

ink

@[simp]

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

ink

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

ink

theorem Finset.powerset_card_disjUnionᵢ {α : Type u_1} (s : Finset α) : Finset.powerset s = Finset.disjUnionᵢ (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))

ink

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

ink

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

ink

@[simp]

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

ink

@[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

ink

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