mathlib3 documentation

data.finset.powerset

The powerset of a finset #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

s.powerset = {val := multiset.pmap finset.mk s.val.powerset _, nodup := _}

@[simp]

theorem finset.mem_powerset {α : Type u_1} {s t : finset α} :

s ∈ t.powerset ↔ s ⊆ t

@[simp, norm_cast]

theorem finset.coe_powerset {α : Type u_1} (s : finset α) :

↑(s.powerset) = coe ⁻¹' 𝒫 ↑s

@[simp]

theorem finset.empty_mem_powerset {α : Type u_1} (s : finset α) :

∅ ∈ s.powerset

@[simp]

theorem finset.mem_powerset_self {α : Type u_1} (s : finset α) :

s ∈ s.powerset

theorem finset.powerset_nonempty {α : Type u_1} (s : finset α) :

s.powerset.nonempty

@[simp]

theorem finset.powerset_mono {α : Type u_1} {s t : finset α} :

s.powerset ⊆ t.powerset ↔ s ⊆ t

theorem finset.powerset_injective {α : Type u_1} :

function.injective finset.powerset

@[simp]

theorem finset.powerset_inj {α : Type u_1} {s t : finset α} :

s.powerset = t.powerset ↔ s = t

@[simp]

theorem finset.powerset_empty {α : Type u_1} :

∅.powerset = {∅}

@[simp]

theorem finset.powerset_eq_singleton_empty {α : Type u_1} {s : finset α} :

s.powerset = {∅} ↔ s = ∅

@[simp]

theorem finset.card_powerset {α : Type u_1} (s : finset α) :

s.powerset.card = 2 ^ s.card

Number of Subsets of a Set

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

theorem finset.powerset_insert {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :

(has_insert.insert a s).powerset = s.powerset ∪ finset.image (has_insert.insert a) s.powerset

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

finset.decidable_exists_of_decidable_subsets = decidable_of_iff (∃ (t : finset α) (hs : t ∈ s.powerset), p t _) finset.decidable_exists_of_decidable_subsets._proof_2

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

finset.decidable_forall_of_decidable_subsets = decidable_of_iff (∀ (t : finset α) (h : t ∈ s.powerset), p t _) finset.decidable_forall_of_decidable_subsets._proof_2

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

finset.decidable_exists_of_decidable_subsets' hu = finset.decidable_exists_of_decidable_subsets

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

finset.decidable_forall_of_decidable_subsets' hu = finset.decidable_forall_of_decidable_subsets

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

s.ssubsets = s.powerset.erase s

@[simp]

theorem finset.mem_ssubsets {α : Type u_1} [decidable_eq α] {s t : finset α} :

t ∈ s.ssubsets ↔ t ⊂ s

theorem finset.empty_mem_ssubsets {α : Type u_1} [decidable_eq α] {s : finset α} (h : s.nonempty) :

∅ ∈ s.ssubsets

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

finset.decidable_exists_of_decidable_ssubsets = decidable_of_iff (∃ (t : finset α) (hs : t ∈ s.ssubsets), p t _) finset.decidable_exists_of_decidable_ssubsets._proof_2

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

finset.decidable_forall_of_decidable_ssubsets = decidable_of_iff (∀ (t : finset α) (h : t ∈ s.ssubsets), p t _) finset.decidable_forall_of_decidable_ssubsets._proof_2

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

finset.decidable_exists_of_decidable_ssubsets' hu = finset.decidable_exists_of_decidable_ssubsets

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

finset.decidable_forall_of_decidable_ssubsets' hu = finset.decidable_forall_of_decidable_ssubsets

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

finset.powerset_len n s = {val := multiset.pmap finset.mk (multiset.powerset_len n s.val) _, nodup := _}

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

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

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

@[simp]

theorem finset.powerset_len_zero {α : Type u_1} (s : finset α) :

finset.powerset_len 0 s = {∅}

@[simp]

theorem finset.powerset_len_empty {α : Type u_1} (n : ℕ) {s : finset α} (h : s.card < n) :

finset.powerset_len n s = ∅

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

theorem finset.powerset_len_succ_insert {α : Type u_1} [decidable_eq α] {x : α} {s : finset α} (h : x ∉ s) (n : ℕ) :

finset.powerset_len n.succ (has_insert.insert x s) = finset.powerset_len n.succ s ∪ finset.image (has_insert.insert x) (finset.powerset_len n s)

theorem finset.powerset_len_nonempty {α : Type u_1} {n : ℕ} {s : finset α} (h : n ≤ s.card) :

(finset.powerset_len n s).nonempty

@[simp]

theorem finset.powerset_len_self {α : Type u_1} (s : finset α) :

finset.powerset_len s.card s = {s}

theorem finset.pairwise_disjoint_powerset_len {α : Type u_1} (s : finset α) :

pairwise (λ (i j : ℕ), disjoint (finset.powerset_len i s) (finset.powerset_len j s))

theorem finset.powerset_card_disj_Union {α : Type u_1} (s : finset α) :

s.powerset = (finset.range (s.card + 1)).disj_Union (λ (i : ℕ), finset.powerset_len i s) _

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)

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

@[simp]

theorem finset.powerset_len_card_add {α : Type u_1} (s : finset α) {i : ℕ} (hi : 0 < i) :

finset.powerset_len (s.card + i) s = ∅

@[simp]

theorem finset.map_val_val_powerset_len {α : Type u_1} (s : finset α) (i : ℕ) :

multiset.map finset.val (finset.powerset_len i s).val = multiset.powerset_len i s.val

theorem finset.powerset_len_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (n : ℕ) (s : finset α) :

finset.powerset_len n (finset.map f s) = finset.map (finset.map_embedding f).to_embedding (finset.powerset_len n s)