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

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

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