Basic lemmas on finite sets

This file contains lemmas on the interaction of various definitions on the Finset type.

For an explanation of Finset design decisions, please see Mathlib/Data/Finset/Defs.lean.

Main declarations

Main definitions

• Finset.choose: Given a proof h of existence and uniqueness of a certain element satisfying a predicate, choose s h returns the element of s satisfying that predicate.

Equivalences between finsets

• The Mathlib/Logic/Equiv/Defs.lean files describe a general type of equivalence, so look in there for any lemmas. There is some API for rewriting sums and products from s to t given that s ≃ t. TODO: examples

Tags

finite sets, finset

Lattice structure

union

@[simp]

theorem Finset.disjUnion_eq_union {α : Type u_1} [DecidableEq α] (s t : Finset α) (h : Disjoint s t) : s.disjUnion t h = s ∪ t

@[simp]

theorem Finset.disjoint_union_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

@[simp]

theorem Finset.disjoint_union_right {α : Type u_1} [DecidableEq α] {s t u : Finset α} : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

inter

theorem Finset.not_disjoint_iff_nonempty_inter {α : Type u_1} [DecidableEq α] {s t : Finset α} : ¬Disjoint s t ↔ (s ∩ t).Nonempty

theorem Finset.Nonempty.not_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} : (s ∩ t).Nonempty → ¬Disjoint s t

Alias of the reverse direction of Finset.not_disjoint_iff_nonempty_inter.

theorem Finset.disjoint_or_nonempty_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) : Disjoint s t ∨ (s ∩ t).Nonempty

theorem Finset.disjoint_of_subset_iff_left_eq_empty {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s ⊆ t) : Disjoint s t ↔ s = ∅

theorem Finset.isDirected_le {α : Type u_1} : IsDirected (Finset α) fun (x1 x2 : Finset α) => x1 ≤ x2

theorem Finset.isDirected_subset {α : Type u_1} : IsDirected (Finset α) fun (x1 x2 : Finset α) => x1 ⊆ x2

erase

@[simp]

theorem Finset.erase_empty {α : Type u_1} [DecidableEq α] (a : α) : ∅.erase a = ∅

theorem Finset.Nontrivial.erase_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (hs : s.Nontrivial) : (s.erase a).Nonempty

@[simp]

theorem Finset.erase_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : (s.erase a).Nonempty ↔ s.Nontrivial

@[simp]

theorem Finset.erase_singleton {α : Type u_1} [DecidableEq α] (a : α) : {a}.erase a = ∅

@[simp]

theorem Finset.erase_insert_eq_erase {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : (insert a s).erase a = s.erase a

theorem Finset.erase_insert {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) : (insert a s).erase a = s

theorem Finset.erase_insert_of_ne {α : Type u_1} [DecidableEq α] {a b : α} {s : Finset α} (h : a ≠ b) : (insert a s).erase b = insert a (s.erase b)

theorem Finset.erase_cons_of_ne {α : Type u_1} [DecidableEq α] {a b : α} {s : Finset α} (ha : a ∉ s) (hb : a ≠ b) : (Finset.cons a s ha).erase b = Finset.cons a (s.erase b) ⋯

@[simp]

theorem Finset.insert_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a ∈ s) : insert a (s.erase a) = s

theorem Finset.erase_eq_iff_eq_insert {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (hs : a ∈ s) (ht : a ∉ t) : s.erase a = t ↔ s = insert a t

theorem Finset.insert_erase_invOn {α : Type u_1} [DecidableEq α] {a : α} : Set.InvOn (insert a) (fun (s : Finset α) => s.erase a) {s : Finset α | a ∈ s} {s : Finset α | a ∉ s}

theorem Finset.erase_ssubset {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∈ s) : s.erase a ⊂ s

theorem Finset.ssubset_iff_exists_subset_erase {α : Type u_1} [DecidableEq α] {s t : Finset α} : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a

theorem Finset.erase_ssubset_insert {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : s.erase a ⊂ insert a s

theorem Finset.erase_cons {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (h : a ∉ s) : (Finset.cons a s h).erase a = s

theorem Finset.subset_insert_iff {α : Type u_1} [DecidableEq α] {a : α} {s t : Finset α} : s ⊆ insert a t ↔ s.erase a ⊆ t

theorem Finset.erase_insert_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).erase a ⊆ s

theorem Finset.insert_erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : s ⊆ insert a (s.erase a)

theorem Finset.subset_insert_iff_of_not_mem {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t

theorem Finset.erase_subset_iff_of_mem {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∈ t) : s.erase a ⊆ t ↔ s ⊆ t

theorem Finset.erase_injOn' {α : Type u_1} [DecidableEq α] (a : α) : Set.InjOn (fun (s : Finset α) => s.erase a) {s : Finset α | a ∈ s}

theorem Finset.Nontrivial.exists_cons_eq {α : Type u_1} {s : Finset α} (hs : s.Nontrivial) : ∃ (t : Finset α) (a : α) (ha : a ∉ t) (b : α) (hb : b ∉ t) (hab : ¬a = b), Finset.cons a (Finset.cons b t hb) ⋯ = s

sdiff

theorem Finset.erase_sdiff_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (hab : a ≠ b) (hb : b ∈ s) : s.erase a \ s.erase b = {b}

theorem Finset.sdiff_singleton_eq_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : s \ {a} = s.erase a

theorem Finset.erase_eq {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : s.erase a = s \ {a}

theorem Finset.disjoint_erase_comm {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} : Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

theorem Finset.disjoint_insert_erase {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : a ∉ t) : Disjoint (s.erase a) (insert a t) ↔ Disjoint s t

theorem Finset.disjoint_erase_insert {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : a ∉ s) : Disjoint (insert a s) (t.erase a) ↔ Disjoint s t

theorem Finset.disjoint_of_erase_left {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : a ∉ t) (hst : Disjoint (s.erase a) t) : Disjoint s t

theorem Finset.disjoint_of_erase_right {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (ha : a ∉ s) (hst : Disjoint s (t.erase a)) : Disjoint s t

theorem Finset.inter_erase {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) : s ∩ t.erase a = (s ∩ t).erase a

@[simp]

theorem Finset.erase_inter {α : Type u_1} [DecidableEq α] (a : α) (s t : Finset α) : s.erase a ∩ t = (s ∩ t).erase a

theorem Finset.erase_sdiff_comm {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) : s.erase a \ t = (s \ t).erase a

theorem Finset.erase_inter_comm {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) : s.erase a ∩ t = s ∩ t.erase a

theorem Finset.erase_union_distrib {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) : (s ∪ t).erase a = s.erase a ∪ t.erase a

theorem Finset.insert_inter_distrib {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) : insert a (s ∩ t) = insert a s ∩ insert a t

theorem Finset.erase_sdiff_distrib {α : Type u_1} [DecidableEq α] (s t : Finset α) (a : α) : (s \ t).erase a = s.erase a \ t.erase a

theorem Finset.erase_union_of_mem {α : Type u_1} [DecidableEq α] {t : Finset α} {a : α} (ha : a ∈ t) (s : Finset α) : s.erase a ∪ t = s ∪ t

theorem Finset.union_erase_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) (t : Finset α) : s ∪ t.erase a = s ∪ t

@[simp, deprecated Finset.erase_eq_of_not_mem]

theorem Finset.sdiff_singleton_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∉ s) : s \ {a} = s

theorem Finset.sdiff_union_erase_cancel {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (hts : t ⊆ s) (ha : a ∈ t) : s \ t ∪ t.erase a = s.erase a

theorem Finset.sdiff_insert {α : Type u_1} [DecidableEq α] (s t : Finset α) (x : α) : s \ insert x t = (s \ t).erase x

theorem Finset.sdiff_insert_insert_of_mem_of_not_mem {α : Type u_1} [DecidableEq α] {s t : Finset α} {x : α} (hxs : x ∈ s) (hxt : x ∉ t) : insert x (s \ insert x t) = s \ t

theorem Finset.sdiff_erase {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∈ s) : s \ t.erase a = insert a (s \ t)

theorem Finset.sdiff_erase_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : s \ s.erase a = {a}

theorem Finset.erase_eq_empty_iff {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : s.erase a = ∅ ↔ s = ∅ ∨ s = {a}

theorem Finset.sdiff_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} : Disjoint (t \ s) s

theorem Finset.disjoint_sdiff {α : Type u_1} [DecidableEq α] {s t : Finset α} : Disjoint s (t \ s)

theorem Finset.disjoint_sdiff_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) : Disjoint (s \ t) (s ∩ t)

attach

@[simp]

theorem Finset.attach_empty {α : Type u_1} : ∅.attach = ∅

@[simp]

theorem Finset.attach_nonempty_iff {α : Type u_1} {s : Finset α} : s.attach.Nonempty ↔ s.Nonempty

theorem Finset.Nonempty.attach {α : Type u_1} {s : Finset α} : s.Nonempty → s.attach.Nonempty

Alias of the reverse direction of Finset.attach_nonempty_iff.

@[simp]

theorem Finset.attach_eq_empty_iff {α : Type u_1} {s : Finset α} : s.attach = ∅ ↔ s = ∅

filter

theorem Finset.filter_singleton {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) : Finset.filter p {a} = if p a then {a} else ∅

theorem Finset.filter_cons_of_pos {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (s : Finset α) (ha : a ∉ s) (hp : p a) : Finset.filter p (Finset.cons a s ha) = Finset.cons a (Finset.filter p s) ⋯

theorem Finset.filter_cons_of_neg {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (s : Finset α) (ha : a ∉ s) (hp : ¬p a) : Finset.filter p (Finset.cons a s ha) = Finset.filter p s

theorem Finset.disjoint_filter {α : Type u_1} {s : Finset α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] : Disjoint (Finset.filter p s) (Finset.filter q s) ↔ ∀ x ∈ s, p x → ¬q x

theorem Finset.disjoint_filter_filter' {α : Type u_1} (s t : Finset α) {p q : α → Prop} [DecidablePred p] [DecidablePred q] (h : Disjoint p q) : Disjoint (Finset.filter p s) (Finset.filter q t)

theorem Finset.disjoint_filter_filter_neg {α : Type u_1} (s t : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] : Disjoint (Finset.filter p s) (Finset.filter (fun (a : α) => ¬p a) t)

@[deprecated Finset.disjoint_filter_filter_neg]

theorem Finset.filter_inter_filter_neg_eq {α : Type u_1} (s t : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] : Disjoint (Finset.filter p s) (Finset.filter (fun (a : α) => ¬p a) t)

Alias of Finset.disjoint_filter_filter_neg.

theorem Finset.filter_disj_union {α : Type u_1} (p : α → Prop) [DecidablePred p] (s t : Finset α) (h : Disjoint s t) : Finset.filter p (s.disjUnion t h) = (Finset.filter p s).disjUnion (Finset.filter p t) ⋯

theorem Finset.filter_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] {a : α} (s : Finset α) (ha : a ∉ s) : Finset.filter p (Finset.cons a s ha) = if p a then Finset.cons a (Finset.filter p s) ⋯ else Finset.filter p s

theorem Finset.filter_union {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s₁ s₂ : Finset α) : Finset.filter p (s₁ ∪ s₂) = Finset.filter p s₁ ∪ Finset.filter p s₂

theorem Finset.filter_union_right {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) : Finset.filter p s ∪ Finset.filter q s = Finset.filter (fun (x : α) => p x ∨ q x) s

theorem Finset.filter_mem_eq_inter {α : Type u_1} [DecidableEq α] {s t : Finset α} [(i : α) → Decidable (i ∈ t)] : Finset.filter (fun (i : α) => i ∈ t) s = s ∩ t

theorem Finset.filter_inter_distrib {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s t : Finset α) : Finset.filter p (s ∩ t) = Finset.filter p s ∩ Finset.filter p t

theorem Finset.filter_inter {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s t : Finset α) : Finset.filter p s ∩ t = Finset.filter p (s ∩ t)

theorem Finset.inter_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s t : Finset α) : s ∩ Finset.filter p t = Finset.filter p (s ∩ t)

theorem Finset.filter_insert {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (a : α) (s : Finset α) : Finset.filter p (insert a s) = if p a then insert a (Finset.filter p s) else Finset.filter p s

theorem Finset.filter_erase {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (a : α) (s : Finset α) : Finset.filter p (s.erase a) = (Finset.filter p s).erase a

theorem Finset.filter_or {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) : Finset.filter (fun (a : α) => p a ∨ q a) s = Finset.filter p s ∪ Finset.filter q s

theorem Finset.filter_and {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) : Finset.filter (fun (a : α) => p a ∧ q a) s = Finset.filter p s ∩ Finset.filter q s

theorem Finset.filter_not {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s : Finset α) : Finset.filter (fun (a : α) => ¬p a) s = s \ Finset.filter p s

theorem Finset.filter_and_not {α : Type u_1} [DecidableEq α] (s : Finset α) (p q : α → Prop) [DecidablePred p] [DecidablePred q] : Finset.filter (fun (a : α) => p a ∧ ¬q a) s = Finset.filter p s \ Finset.filter q s

theorem Finset.sdiff_eq_filter {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : s₁ \ s₂ = Finset.filter (fun (x : α) => x ∉ s₂) s₁

theorem Finset.subset_union_elim {α : Type u_1} [DecidableEq α] {s : Finset α} {t₁ t₂ : Set α} (h : ↑s ⊆ t₁ ∪ t₂) : ∃ (s₁ : Finset α) (s₂ : Finset α), s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁

theorem Finset.filter_eq {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) : Finset.filter (Eq b) s = if b ∈ s then {b} else ∅

After filtering out everything that does not equal a given value, at most that value remains.

This is equivalent to filter_eq' with the equality the other way.

theorem Finset.filter_eq' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) : Finset.filter (fun (a : β) => a = b) s = if b ∈ s then {b} else ∅

After filtering out everything that does not equal a given value, at most that value remains.

This is equivalent to filter_eq with the equality the other way.

theorem Finset.filter_ne {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) : Finset.filter (fun (a : β) => b ≠ a) s = s.erase b

theorem Finset.filter_ne' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) : Finset.filter (fun (a : β) => a ≠ b) s = s.erase b

theorem Finset.filter_union_filter_of_codisjoint {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) (h : Codisjoint p q) : Finset.filter p s ∪ Finset.filter q s = s

theorem Finset.filter_union_filter_neg_eq {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] [(x : α) → Decidable ¬p x] (s : Finset α) : Finset.filter p s ∪ Finset.filter (fun (a : α) => ¬p a) s = s

range

@[simp]

theorem Finset.range_filter_eq {n m : ℕ} : Finset.filter (fun (x : ℕ) => x = m) (Finset.range n) = if m < n then {m} else ∅

dedup on list and multiset

@[simp]

theorem Multiset.toFinset_add {α : Type u_1} [DecidableEq α] (s t : Multiset α) : (s + t).toFinset = s.toFinset ∪ t.toFinset

@[simp]

theorem Multiset.toFinset_nsmul {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ℕ) : n ≠ 0 → (n • s).toFinset = s.toFinset

theorem Multiset.toFinset_eq_singleton_iff {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : s.toFinset = {a} ↔ Multiset.card s ≠ 0 ∧ s = Multiset.card s • {a}

@[simp]

theorem Multiset.toFinset_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : (s ∩ t).toFinset = s.toFinset ∩ t.toFinset

@[simp]

theorem Multiset.toFinset_union {α : Type u_1} [DecidableEq α] (s t : Multiset α) : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

@[simp]

theorem Multiset.toFinset_eq_empty {α : Type u_1} [DecidableEq α] {m : Multiset α} : m.toFinset = ∅ ↔ m = 0

@[simp]

theorem Multiset.toFinset_nonempty {α : Type u_1} [DecidableEq α] {s : Multiset α} : s.toFinset.Nonempty ↔ s ≠ 0

theorem Multiset.Aesop.toFinset_nonempty_of_ne {α : Type u_1} [DecidableEq α] {s : Multiset α} : s ≠ 0 → s.toFinset.Nonempty

Alias of the reverse direction of Multiset.toFinset_nonempty.

@[simp]

theorem Multiset.toFinset_filter {α : Type u_1} [DecidableEq α] (s : Multiset α) (p : α → Prop) [DecidablePred p] : (Multiset.filter p s).toFinset = Finset.filter p s.toFinset

@[simp]

theorem List.toFinset_union {α : Type u_1} [DecidableEq α] (l l' : List α) : (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset

@[simp]

theorem List.toFinset_inter {α : Type u_1} [DecidableEq α] (l l' : List α) : (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset

theorem List.Aesop.toFinset_nonempty_of_ne {α : Type u_1} [DecidableEq α] (l : List α) : l ≠ [] → l.toFinset.Nonempty

Alias of the reverse direction of List.toFinset_nonempty_iff.

@[simp]

theorem List.toFinset_filter {α : Type u_1} [DecidableEq α] (s : List α) (p : α → Bool) : (List.filter p s).toFinset = Finset.filter (fun (x : α) => p x = true) s.toFinset

@[simp]

theorem Finset.toList_eq_nil {α : Type u_1} {s : Finset α} : s.toList = [] ↔ s = ∅

theorem Finset.empty_toList {α : Type u_1} {s : Finset α} : s.toList.isEmpty = true ↔ s = ∅

@[simp]

theorem Finset.toList_empty {α : Type u_1} : ∅.toList = []

theorem Finset.Nonempty.toList_ne_nil {α : Type u_1} {s : Finset α} (hs : s.Nonempty) : s.toList ≠ []

theorem Finset.Nonempty.not_empty_toList {α : Type u_1} {s : Finset α} (hs : s.Nonempty) : ¬s.toList.isEmpty = true

choose

def Finset.chooseX {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : { a : α // a ∈ l ∧ p a }

Given a finset l and a predicate p, associate to a proof that there is a unique element of l satisfying p this unique element, as an element of the corresponding subtype.

Equations

• Finset.chooseX p l hp = Multiset.chooseX p l.val hp

def Finset.choose {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : α

Given a finset l and a predicate p, associate to a proof that there is a unique element of l satisfying p this unique element, as an element of the ambient type.

Equations

• Finset.choose p l hp = ↑(Finset.chooseX p l hp)

theorem Finset.choose_spec {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : Finset.choose p l hp ∈ l ∧ p (Finset.choose p l hp)

theorem Finset.choose_mem {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : Finset.choose p l hp ∈ l

theorem Finset.choose_property {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : Finset α) (hp : ∃! a : α, a ∈ l ∧ p a) : p (Finset.choose p l hp)

def Equiv.Finset.union {α : Type u_1} [DecidableEq α] (s t : Finset α) (h : Disjoint s t) : { x : α // x ∈ s } ⊕ { x : α // x ∈ t } ≃ { x : α // x ∈ s ∪ t }

The disjoint union of finsets is a sum

Equations

• Equiv.Finset.union s t h = ((Equiv.Set.ofEq ⋯).trans (Equiv.Set.union ⋯)).symm

@[simp]

theorem Equiv.Finset.union_symm_inl {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (x : { x : α // x ∈ s }) : (Equiv.Finset.union s t h) (Sum.inl x) = ⟨↑x, ⋯⟩

@[simp]

theorem Equiv.Finset.union_symm_inr {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (y : { x : α // x ∈ t }) : (Equiv.Finset.union s t h) (Sum.inr y) = ⟨↑y, ⋯⟩

def Equiv.piFinsetUnion {ι : Type u_5} [DecidableEq ι] (α : ι → Type u_4) {s t : Finset ι} (h : Disjoint s t) : ((i : { x : ι // x ∈ s }) → α ↑i) × ((i : { x : ι // x ∈ t }) → α ↑i) ≃ ((i : { x : ι // x ∈ s ∪ t }) → α ↑i)

The type of dependent functions on the disjoint union of finsets s ∪ t is equivalent to the type of pairs of functions on s and on t. This is similar to Equiv.sumPiEquivProdPi.

Equations

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

@[simp]

theorem Multiset.toFinset_replicate {α : Type u_1} [DecidableEq α] (n : ℕ) (a : α) : (Multiset.replicate n a).toFinset = if n = 0 then ∅ else {a}