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 file describes 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 #

source

@[simp]

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

s.disjUnion t h = s ∪ t

source

@[simp]

theorem Finset.disjoint_union_left {α : Type u_1} [DecidableEq α] {s t u : Finset α} :

Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

source

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

source

theorem Finset.not_disjoint_iff_nonempty_inter {α : Type u_1} [DecidableEq α] {s t : Finset α} :

¬Disjoint s t ↔ (s ∩ t).Nonempty

source

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.

source

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

Disjoint s t ∨ (s ∩ t).Nonempty

source

theorem Finset.disjoint_of_subset_iff_left_eq_empty {α : Type u_1} {s t : Finset α} (h : s ⊆ t) :

Disjoint s t ↔ s = ∅

source

theorem Finset.pairwiseDisjoint_iff {α : Type u_1} [DecidableEq α] {ι : Type u_4} {s : Set ι} {f : ι → Finset α} :

s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

source

instance Finset.isDirected_le {α : Type u_1} :

IsDirectedOrder (Finset α)

source

instance Finset.isDirected_subset {α : Type u_1} :

IsDirected (Finset α) fun (x1 x2 : Finset α) => x1 ⊆ x2

erase #

source

@[simp]

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

∅.erase a = ∅

source

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

(s.erase a).Nonempty

source

@[simp]

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

(s.erase a).Nonempty ↔ s.Nontrivial

source

@[simp]

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

{a}.erase a = ∅

source

@[simp]

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

(insert a s).erase a = s.erase a

source

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

(insert a s).erase a = s

source

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)

source

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

(cons a s ha).erase b = cons a (s.erase b) ⋯

source

@[simp]

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

insert a (s.erase a) = s

source

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

source

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}

source

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

s.erase a ⊂ s

source

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

s.erase a ∪ {a} = s

source

theorem Finset.ssubset_iff_exists_subset_erase {α : Type u_1} [DecidableEq α] {s t : Finset α} :

s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a

source

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

s.erase a ⊂ insert a s

source

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

(cons a s h).erase a = s

source

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

s ⊆ insert a t ↔ s.erase a ⊆ t

source

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

(insert a s).erase a ⊆ s

source

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

s ⊆ insert a (s.erase a)

source

theorem Finset.subset_insert_iff_of_notMem {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∉ s) :

s ⊆ insert a t ↔ s ⊆ t

source

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

s.erase a ⊆ t ↔ s ⊆ t

source

theorem Finset.erase_injOn' {α : Type u_1} [DecidableEq α] (a : α) :

Set.InjOn (fun (s : Finset α) => s.erase a) {s : Finset α | a ∈ s}

source

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), cons a (cons b t hb) ⋯ = s

sdiff #

source

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}

source

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

s \ {a} = s.erase a

source

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

s.erase a = s \ {a}

source

theorem Finset.disjoint_erase_comm {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :

Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

source

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

source

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

source

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

source

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

source

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

s ∩ t.erase a = (s ∩ t).erase a

source

@[simp]

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

s.erase a ∩ t = (s ∩ t).erase a

source

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

s.erase a \ t = (s \ t).erase a

source

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

s.erase a ∩ t = s ∩ t.erase a

source

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

(s ∪ t).erase a = s.erase a ∪ t.erase a

source

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

insert a (s ∩ t) = insert a s ∩ insert a t

source

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

(s \ t).erase a = s.erase a \ t.erase a

source

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

s.erase a ∪ t = s ∪ t

source

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

s ∪ t.erase a = s ∪ t

source

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

source

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

s \ insert x t = (s \ t).erase x

source

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

insert x (s \ insert x t) = s \ t

source

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

s \ t.erase a = insert a (s \ t)

source

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

s \ s.erase a = {a}

source

theorem Finset.erase_eq_empty_iff {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :

s.erase a = ∅ ↔ s = ∅ ∨ s = {a}

source

theorem Finset.sdiff_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} :

Disjoint (t \ s) s

source

theorem Finset.disjoint_sdiff {α : Type u_1} [DecidableEq α] {s t : Finset α} :

Disjoint s (t \ s)

source

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

Disjoint (s \ t) (s ∩ t)

attach #

source

@[simp]

theorem Finset.attach_empty {α : Type u_1} :

∅.attach = ∅

source

@[simp]

theorem Finset.attach_nonempty_iff {α : Type u_1} {s : Finset α} :

s.attach.Nonempty ↔ s.Nonempty

source

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

s.Nonempty → s.attach.Nonempty

Alias of the reverse direction of Finset.attach_nonempty_iff.

source

@[simp]

theorem Finset.attach_eq_empty_iff {α : Type u_1} {s : Finset α} :

s.attach = ∅ ↔ s = ∅

filter #

source

theorem Finset.filter_singleton {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) :

filter p {a} = if p a then {a} else ∅

source

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

filter p (cons a s ha) = cons a (filter p s) ⋯

source

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

filter p (cons a s ha) = filter p s

source

theorem Finset.disjoint_filter {α : Type u_1} {s : Finset α} {p q : α → Prop} [DecidablePred p] [DecidablePred q] :

Disjoint (filter p s) (filter q s) ↔ ∀ x ∈ s, p x → ¬q x

source

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

Disjoint (filter p s) (filter q t)

source

theorem Finset.disjoint_filter_filter_not {α : Type u_1} (s t : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] :

Disjoint (filter p s) (filter (fun (a : α) => ¬p a) t)

source

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

filter p (s.disjUnion t h) = (filter p s).disjUnion (filter p t) ⋯

source

theorem Finset.filter_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] {a : α} (s : Finset α) (ha : a ∉ s) :

filter p (cons a s ha) = if p a then cons a (filter p s) ⋯ else filter p s

source

@[simp]

theorem Finset.disjoint_disjUnion_left {α : Type u_1} {s t u : Finset α} (h : Disjoint s t) :

Disjoint (s.disjUnion t h) u ↔ Disjoint s u ∧ Disjoint t u

source

@[simp]

theorem Finset.disjoint_disjUnion_right {α : Type u_1} {s t u : Finset α} (h : Disjoint t u) :

Disjoint s (t.disjUnion u h) ↔ Disjoint s t ∧ Disjoint s u

source

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

filter p (s₁ ∪ s₂) = filter p s₁ ∪ filter p s₂

source

theorem Finset.filter_union_right {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) :

filter p s ∪ filter q s = filter (fun (x : α) => p x ∨ q x) s

source

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

filter (fun (i : α) => i ∈ t) s = s ∩ t

source

theorem Finset.filter_notMem_eq_sdiff {α : Type u_1} [DecidableEq α] {s t : Finset α} [(i : α) → Decidable (i ∉ t)] :

filter (fun (i : α) => i ∉ t) s = s \ t

source

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

filter p (s ∩ t) = filter p s ∩ filter p t

source

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

filter p s ∩ t = filter p (s ∩ t)

source

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

s ∩ filter p t = filter p (s ∩ t)

source

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

filter p (insert a s) = if p a then insert a (filter p s) else filter p s

source

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

filter p (s.erase a) = (filter p s).erase a

source

theorem Finset.filter_or {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) :

filter (fun (a : α) => p a ∨ q a) s = filter p s ∪ filter q s

source

theorem Finset.filter_and {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] [DecidableEq α] (s : Finset α) :

filter (fun (a : α) => p a ∧ q a) s = filter p s ∩ filter q s

source

theorem Finset.filter_not {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] (s : Finset α) :

filter (fun (a : α) => ¬p a) s = s \ filter p s

source

theorem Finset.filter_and_not {α : Type u_1} [DecidableEq α] (s : Finset α) (p q : α → Prop) [DecidablePred p] [DecidablePred q] :

filter (fun (a : α) => p a ∧ ¬q a) s = filter p s \ filter q s

source

theorem Finset.sdiff_eq_filter {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :

s₁ \ s₂ = filter (fun (x : α) => x ∉ s₂) s₁

source

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₁

source

theorem Finset.filter_eq {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :

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.

source

theorem Finset.filter_eq' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :

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.

source

theorem Finset.filter_ne {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :

filter (fun (a : β) => b ≠ a) s = s.erase b

source

theorem Finset.filter_ne' {β : Type u_2} [DecidableEq β] (s : Finset β) (b : β) :

filter (fun (a : β) => a ≠ b) s = s.erase b

source

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

filter p s ∪ filter q s = s

source

theorem Finset.filter_union_filter_not_eq {α : Type u_1} (p : α → Prop) [DecidablePred p] [DecidableEq α] [(x : α) → Decidable ¬p x] (s : Finset α) :

filter p s ∪ filter (fun (a : α) => ¬p a) s = s

range #

source

@[simp]

theorem Finset.range_filter_eq {n m : ℕ} :

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

source

@[simp]

theorem Finset.range_inter_range (m n : ℕ) :

range m ∩ range n = range (min m n)

source

@[simp]

theorem Finset.range_union_range (m n : ℕ) :

range m ∪ range n = range (max m n)

dedup on list and multiset #

source

@[simp]

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

(s + t).toFinset = s.toFinset ∪ t.toFinset

source

@[simp]

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

(s ∩ t).toFinset = s.toFinset ∩ t.toFinset

source

@[simp]

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

(s ∪ t).toFinset = s.toFinset ∪ t.toFinset

source

@[simp]

theorem Multiset.toFinset_eq_empty {α : Type u_1} [DecidableEq α] {m : Multiset α} :

m.toFinset = ∅ ↔ m = 0

source

@[simp]

theorem Multiset.toFinset_nonempty {α : Type u_1} [DecidableEq α] {s : Multiset α} :

s.toFinset.Nonempty ↔ s ≠ 0

source

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.

source

@[simp]

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

(filter p s).toFinset = Finset.filter p s.toFinset

source

@[simp]

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

(l ∪ l').toFinset = l.toFinset ∪ l'.toFinset

source

@[simp]

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

(l ∩ l').toFinset = l.toFinset ∩ l'.toFinset

source

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.

source

@[simp]

theorem List.toFinset_filter {α : Type u_1} [DecidableEq α] (s : List α) (p : α → Bool) :

(filter p s).toFinset = Finset.filter (fun (x : α) => p x = true) s.toFinset

source

@[simp]

theorem Finset.toList_eq_nil {α : Type u_1} {s : Finset α} :

s.toList = [] ↔ s = ∅

source

theorem Finset.empty_toList {α : Type u_1} {s : Finset α} :

s.toList.isEmpty = true ↔ s = ∅

source

@[simp]

theorem Finset.toList_empty {α : Type u_1} :

∅.toList = []

source

theorem Finset.Nonempty.toList_ne_nil {α : Type u_1} {s : Finset α} (hs : s.Nonempty) :

s.toList ≠ []

source

theorem Finset.Nonempty.not_empty_toList {α : Type u_1} {s : Finset α} (hs : s.Nonempty) :

¬s.toList.isEmpty = true

choose #

source

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

Instances For

source

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)

Instances For

source

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

choose p l hp ∈ l ∧ p (choose p l hp)

source

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

choose p l hp ∈ l

source

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

p (choose p l hp)

source

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

choose p l hp = a ↔ a ∈ l ∧ p a

source

def Equiv.Finset.union {α : Type u_1} [DecidableEq α] (s t : Finset α) (h : Disjoint s t) :

↥s ⊕ ↥t ≃ ↥(s ∪ t)

The disjoint union of finsets is a sum

Equations

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

Instances For

source

@[simp]

theorem Equiv.Finset.union_inl {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (x : ↥s) :

(union s t h) (Sum.inl x) = ⟨↑x, ⋯⟩

source

@[simp]

theorem Equiv.Finset.union_inr {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (y : ↥t) :

(union s t h) (Sum.inr y) = ⟨↑y, ⋯⟩

source

@[simp]

theorem Equiv.Finset.union_symm_left {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) {i : α} (hi : i ∈ s) (hi' : i ∈ s ∪ t) :

(union s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩

source

@[simp]

theorem Equiv.Finset.union_symm_right {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) {i : α} (hi : i ∈ t) (hi' : i ∈ s ∪ t) :

(union s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩

source

def Equiv.Finset.disjUnionEquiv {α : Type u_1} [DecidableEq α] (s t : Finset α) (h : Disjoint s t) :

↥s ⊕ ↥t ≃ ↥(s.disjUnion t h)

The disjoint union of finsets is a sum

Equations

Equiv.Finset.disjUnionEquiv s t h = ((Equiv.setCongr ⋯).trans (Equiv.Set.union ⋯)).symm

Instances For

source

@[simp]

theorem Equiv.Finset.disjUnionEquiv_inl {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (x : ↥s) :

(disjUnionEquiv s t h) (Sum.inl x) = ⟨↑x, ⋯⟩

source

@[simp]

theorem Equiv.Finset.disjUnionEquiv_inr {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (y : ↥t) :

(disjUnionEquiv s t h) (Sum.inr y) = ⟨↑y, ⋯⟩

source

@[simp]

theorem Equiv.Finset.disjUnionEquiv_symm_left {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) {i : α} (hi : i ∈ s) (hi' : i ∈ s.disjUnion t h) :

(disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩

source

@[simp]

theorem Equiv.Finset.disjUnionEquiv_symm_right {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) {i : α} (hi : i ∈ t) (hi' : i ∈ s.disjUnion t h) :

(disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩

source

def Equiv.piFinsetUnion {ι : Type u_5} [DecidableEq ι] (α : ι → Type u_4) {s t : Finset ι} (h : Disjoint s t) :

((i : ↥s) → α ↑i) × ((i : ↥t) → α ↑i) ≃ ((i : ↥(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

Equiv.piFinsetUnion α h = (Equiv.sumPiEquivProdPi fun (b : ↥s ⊕ ↥t) => α ↑((Equiv.Finset.union s t h) b)).symm.trans (Equiv.piCongrLeft (fun (i : ↥(s ∪ t)) => α ↑i) (Equiv.Finset.union s t h))

Instances For

source

theorem Equiv.piFinsetUnion_left {ι : Type u_5} [DecidableEq ι] (α : ι → Type u_4) {s t : Finset ι} (h : Disjoint s t) {f : (i : ↥s) → α ↑i} {g : (i : ↥t) → α ↑i} {i : ι} (hi : i ∈ s) (hi' : i ∈ s ∪ t) :

(piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩

source

theorem Equiv.piFinsetUnion_right {ι : Type u_5} [DecidableEq ι] (α : ι → Type u_4) {s t : Finset ι} (h : Disjoint s t) {f : (i : ↥s) → α ↑i} {g : (i : ↥t) → α ↑i} {i : ι} (hi : i ∈ t) (hi' : i ∈ s ∪ t) :