mathlib documentation

data.finset.powerset

The powerset of a finset #

powerset #

source
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
source
@[simp]
theorem finset.mem_powerset {α : Type u_1} {s t : finset α} :
s ∈ t.powerset ↔ s ⊆ t
source
@[simp]
theorem finset.empty_mem_powerset {α : Type u_1} (s : finset α) :
∅ ∈ s.powerset
source
@[simp]
theorem finset.mem_powerset_self {α : Type u_1} (s : finset α) :
s ∈ s.powerset
source
@[simp]
theorem finset.powerset_empty {α : Type u_1} :
∅.powerset = {∅}
source
@[simp]
theorem finset.powerset_mono {α : Type u_1} {s t : finset α} :
s.powerset ⊆ t.powerset ↔ s ⊆ t
source
@[simp]
theorem finset.card_powerset {α : Type u_1} (s : finset α) :
s.powerset.card = 2 ^ s.card

Number of Subsets of a Set

source
theorem finset.not_mem_of_mem_powerset_of_not_mem {α : Type u_1} {s t : finset α} {a : α} (ht : t ∈ s.powerset) (h : a ∉ s) :
a ∉ t
source
theorem finset.powerset_insert {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :
(insert a s).powerset = s.powerset ∪ finset.image (insert a) s.powerset
source
@[protected, instance]
def finset.decidable_exists_of_decidable_subsets {α : 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
source
@[protected, instance]
def finset.decidable_forall_of_decidable_subsets {α : 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
source
def finset.decidable_exists_of_decidable_subsets' {α : Type u_1} {s : finset α} {p : finset α → Prop} (hu : Π (t : finset α), t ⊆ s → decidable (p t)) :
decidable (∃ (t : finset α) (h : t ⊆ s), p t)

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

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

Equations
source
def finset.ssubsets {α : Type u_1} [decidable_eq α] (s : finset α) :
finset (finset α)

For s a finset, s.ssubsets is the finset comprising strict subsets of s.

Equations
source
@[simp]
theorem finset.mem_ssubsets {α : Type u_1} [decidable_eq α] {s t : finset α} :
t ∈ s.ssubsets ↔ t ⊂ s
source
theorem finset.empty_mem_ssubsets {α : Type u_1} [decidable_eq α] {s : finset α} (h : s.nonempty) :
∅ ∈ s.ssubsets
source
@[protected, instance]
def finset.decidable_exists_of_decidable_ssubsets {α : Type u_1} [decidable_eq α] {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
source
@[protected, instance]
def finset.decidable_forall_of_decidable_ssubsets {α : Type u_1} [decidable_eq α] {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
source
def finset.decidable_exists_of_decidable_ssubsets' {α : Type u_1} [decidable_eq α] {s : finset α} {p : finset α → Prop} (hu : Π (t : finset α), t ⊂ s → decidable (p t)) :
decidable (∃ (t : finset α) (h : t ⊂ s), p t)

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

Equations
source
def finset.decidable_forall_of_decidable_ssubsets' {α : Type u_1} [decidable_eq α] {s : finset α} {p : finset α → Prop} (hu : Π (t : finset α), t ⊂ s → decidable (p t)) :
decidable (∀ (t : finset α), t ⊂ s → p t)

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

Equations
source
def finset.powerset_len {α : Type u_1} (n : ℕ) (s : finset α) :
finset (finset α)

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

Equations
source
theorem finset.mem_powerset_len {α : Type u_1} {n : ℕ} {s t : finset α} :
s ∈ finset.powerset_len n t ↔ s ⊆ t ∧ s.card = n

Formula for the Number of Combinations

source
@[simp]
theorem finset.powerset_len_mono {α : Type u_1} {n : ℕ} {s t : finset α} (h : s ⊆ t) :
finset.powerset_len n s ⊆ finset.powerset_len n t
source
@[simp]
theorem finset.card_powerset_len {α : Type u_1} (n : ℕ) (s : finset α) :
(finset.powerset_len n s).card = s.card.choose n

Formula for the Number of Combinations

source
@[simp]
theorem finset.powerset_len_zero {α : Type u_1} (s : finset α) :
finset.powerset_len 0 s = {∅}
source
@[simp]
theorem finset.powerset_len_empty {α : Type u_1} (n : ℕ) {s : finset α} (h : s.card < n) :
finset.powerset_len n s = ∅
source
theorem finset.powerset_len_eq_filter {α : Type u_1} {n : ℕ} {s : finset α} :
finset.powerset_len n s = finset.filter (λ (x : finset α), x.card = n) s.powerset
source
theorem finset.powerset_len_succ_insert {α : Type u_1} [decidable_eq α] {x : α} {s : finset α} (h : x ∉ s) (n : ℕ) :
finset.powerset_len n.succ (insert x s) = finset.powerset_len n.succ s ∪ finset.image (insert x) (finset.powerset_len n s)
source
theorem finset.powerset_len_nonempty {α : Type u_1} {n : ℕ} {s : finset α} (h : n < s.card) :
(finset.powerset_len n s).nonempty
source
@[simp]
theorem finset.powerset_len_self {α : Type u_1} (s : finset α) :
finset.powerset_len s.card s = {s}
source
theorem finset.powerset_card_bUnion {α : Type u_1} [decidable_eq (finset α)] (s : finset α) :
s.powerset = (finset.range (s.card + 1)).bUnion (λ (i : ℕ), finset.powerset_len i s)
source
theorem finset.powerset_len_sup {α : Type u_1} [decidable_eq α] (u : finset α) (n : ℕ) (hn : n < u.card) :
(finset.powerset_len n.succ u).sup id = u