Lemmas about insertion, singleton, and pairs

This file provides extra lemmas about insert, singleton, and pair.

Tags

insert, singleton

Set coercion to a type

Lemmas about insert

insert α s is the set {α} ∪ s.

theorem Set.insert_def {α : Type u} (x : α) (s : Set α) : insert x s = {y : α | y = x ∨ y ∈ s}

@[simp]

theorem Set.subset_insert {α : Type u} (x : α) (s : Set α) : s ⊆ insert x s

theorem Set.mem_insert {α : Type u} (x : α) (s : Set α) : x ∈ insert x s

theorem Set.mem_insert_of_mem {α : Type u} {x : α} {s : Set α} (y : α) : x ∈ s → x ∈ insert y s

theorem Set.eq_or_mem_of_mem_insert {α : Type u} {x a : α} {s : Set α} : x ∈ insert a s → x = a ∨ x ∈ s

theorem Set.mem_of_mem_insert_of_ne {α : Type u} {s : Set α} {a b : α} : b ∈ insert a s → b ≠ a → b ∈ s

theorem Set.eq_of_mem_insert_of_notMem {α : Type u} {s : Set α} {a b : α} : b ∈ insert a s → b ∉ s → b = a

@[deprecated Set.eq_of_mem_insert_of_notMem (since := "2025-05-23")]

theorem Set.eq_of_not_mem_of_mem_insert {α : Type u} {s : Set α} {a b : α} : b ∈ insert a s → b ∉ s → b = a

Alias of Set.eq_of_mem_insert_of_notMem.

@[simp]

theorem Set.mem_insert_iff {α : Type u} {x a : α} {s : Set α} : x ∈ insert a s ↔ x = a ∨ x ∈ s

@[simp]

theorem Set.insert_eq_of_mem {α : Type u} {a : α} {s : Set α} (h : a ∈ s) : insert a s = s

theorem Set.ne_insert_of_notMem {α : Type u} {s : Set α} (t : Set α) {a : α} : a ∉ s → s ≠ insert a t

@[deprecated Set.ne_insert_of_notMem (since := "2025-05-23")]

theorem Set.ne_insert_of_not_mem {α : Type u} {s : Set α} (t : Set α) {a : α} : a ∉ s → s ≠ insert a t

Alias of Set.ne_insert_of_notMem.

@[simp]

theorem Set.insert_eq_self {α : Type u} {s : Set α} {a : α} : insert a s = s ↔ a ∈ s

theorem Set.insert_ne_self {α : Type u} {s : Set α} {a : α} : insert a s ≠ s ↔ a ∉ s

theorem Set.insert_subset_iff {α : Type u} {s t : Set α} {a : α} : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t

theorem Set.insert_subset {α : Type u} {s t : Set α} {a : α} (ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t

theorem Set.insert_subset_insert {α : Type u} {s t : Set α} {a : α} (h : s ⊆ t) : insert a s ⊆ insert a t

@[simp]

theorem Set.insert_subset_insert_iff {α : Type u} {s t : Set α} {a : α} (ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t

theorem Set.subset_insert_iff_of_notMem {α : Type u} {s t : Set α} {a : α} (ha : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t

@[deprecated Set.subset_insert_iff_of_notMem (since := "2025-05-23")]

theorem Set.subset_insert_iff_of_not_mem {α : Type u} {s t : Set α} {a : α} (ha : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t

Alias of Set.subset_insert_iff_of_notMem.

theorem Set.ssubset_iff_insert {α : Type u} {s t : Set α} : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t

theorem HasSubset.Subset.ssubset_of_mem_notMem {α : Type u} {s t : Set α} {a : α} (hst : s ⊆ t) (hat : a ∈ t) (has : a ∉ s) : s ⊂ t

@[deprecated HasSubset.Subset.ssubset_of_mem_notMem (since := "2025-05-23")]

theorem HasSubset.Subset.ssubset_of_mem_not_mem {α : Type u} {s t : Set α} {a : α} (hst : s ⊆ t) (hat : a ∈ t) (has : a ∉ s) : s ⊂ t

Alias of HasSubset.Subset.ssubset_of_mem_notMem.

theorem Set.ssubset_insert {α : Type u} {s : Set α} {a : α} (h : a ∉ s) : s ⊂ insert a s

theorem Set.insert_comm {α : Type u} (a b : α) (s : Set α) : insert a (insert b s) = insert b (insert a s)

theorem Set.insert_idem {α : Type u} (a : α) (s : Set α) : insert a (insert a s) = insert a s

theorem Set.insert_union {α : Type u} {s t : Set α} {a : α} : insert a s ∪ t = insert a (s ∪ t)

@[simp]

theorem Set.union_insert {α : Type u} {s t : Set α} {a : α} : s ∪ insert a t = insert a (s ∪ t)

@[simp]

theorem Set.insert_nonempty {α : Type u} (a : α) (s : Set α) : (insert a s).Nonempty

instance Set.instNonemptyElemInsert {α : Type u} (a : α) (s : Set α) : Nonempty ↑(insert a s)

theorem Set.insert_inter_distrib {α : Type u} (a : α) (s t : Set α) : insert a (s ∩ t) = insert a s ∩ insert a t

theorem Set.insert_union_distrib {α : Type u} (a : α) (s t : Set α) : insert a (s ∪ t) = insert a s ∪ insert a t

theorem Set.forall_of_forall_insert {α : Type u} {P : α → Prop} {a : α} {s : Set α} (H : ∀ x ∈ insert a s, P x) (x : α) (h : x ∈ s) : P x

theorem Set.forall_insert_of_forall {α : Type u} {P : α → Prop} {a : α} {s : Set α} (H : ∀ x ∈ s, P x) (ha : P a) (x : α) (h : x ∈ insert a s) : P x

theorem Set.exists_mem_insert {α : Type u} {P : α → Prop} {a : α} {s : Set α} : (∃ x ∈ insert a s, P x) ↔ P a ∨ ∃ x ∈ s, P x

theorem Set.forall_mem_insert {α : Type u} {P : α → Prop} {a : α} {s : Set α} : (∀ x ∈ insert a s, P x) ↔ P a ∧ ∀ x ∈ s, P x

def Set.subtypeInsertEquivOption {α : Type u} [DecidableEq α] {t : Set α} {x : α} (h : x ∉ t) : { i : α // i ∈ insert x t } ≃ Option { i : α // i ∈ t }

Inserting an element to a set is equivalent to the option type.

Equations

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

Lemmas about singletons

instance Set.instLawfulSingleton {α : Type u} : LawfulSingleton α (Set α)

theorem Set.singleton_def {α : Type u} (a : α) : {a} = insert a ∅

@[simp]

theorem Set.mem_singleton_iff {α : Type u} {a b : α} : a ∈ {b} ↔ a = b

theorem Set.notMem_singleton_iff {α : Type u} {a b : α} : a ∉ {b} ↔ a ≠ b

@[deprecated Set.notMem_singleton_iff (since := "2025-05-23")]

theorem Set.not_mem_singleton_iff {α : Type u} {a b : α} : a ∉ {b} ↔ a ≠ b

Alias of Set.notMem_singleton_iff.

@[simp]

theorem Set.setOf_eq_eq_singleton {α : Type u} {a : α} : {n : α | n = a} = {a}

@[simp]

theorem Set.setOf_eq_eq_singleton' {α : Type u} {a : α} : {x : α | a = x} = {a}

theorem Set.mem_singleton {α : Type u} (a : α) : a ∈ {a}

theorem Set.eq_of_mem_singleton {α : Type u} {x y : α} (h : x ∈ {y}) : x = y

@[simp]

theorem Set.singleton_eq_singleton_iff {α : Type u} {x y : α} : {x} = {y} ↔ x = y

theorem Set.singleton_injective {α : Type u} : Function.Injective singleton

theorem Set.mem_singleton_of_eq {α : Type u} {x y : α} (H : x = y) : x ∈ {y}

theorem Set.insert_eq {α : Type u} (x : α) (s : Set α) : insert x s = {x} ∪ s

@[simp]

theorem Set.singleton_nonempty {α : Type u} (a : α) : {a}.Nonempty

@[simp]

theorem Set.singleton_ne_empty {α : Type u} (a : α) : {a} ≠ ∅

theorem Set.empty_ssubset_singleton {α : Type u} {a : α} : ∅ ⊂ {a}

@[simp]

theorem Set.singleton_subset_iff {α : Type u} {a : α} {s : Set α} : {a} ⊆ s ↔ a ∈ s

theorem Set.singleton_subset_singleton {α : Type u} {a b : α} : {a} ⊆ {b} ↔ a = b

theorem Set.GCongr.singleton_subset_singleton {α : Type u} {a b : α} : a = b → {a} ⊆ {b}

Alias of the reverse direction of Set.singleton_subset_singleton.

theorem Set.set_compr_eq_eq_singleton {α : Type u} {a : α} : {b : α | b = a} = {a}

@[simp]

theorem Set.singleton_union {α : Type u} {s : Set α} {a : α} : {a} ∪ s = insert a s

@[simp]

theorem Set.union_singleton {α : Type u} {s : Set α} {a : α} : s ∪ {a} = insert a s

@[simp]

theorem Set.singleton_inter_nonempty {α : Type u} {s : Set α} {a : α} : ({a} ∩ s).Nonempty ↔ a ∈ s

@[simp]

theorem Set.inter_singleton_nonempty {α : Type u} {s : Set α} {a : α} : (s ∩ {a}).Nonempty ↔ a ∈ s

@[simp]

theorem Set.singleton_inter_eq_empty {α : Type u} {s : Set α} {a : α} : {a} ∩ s = ∅ ↔ a ∉ s

@[simp]

theorem Set.inter_singleton_eq_empty {α : Type u} {s : Set α} {a : α} : s ∩ {a} = ∅ ↔ a ∉ s

theorem Set.notMem_singleton_empty {α : Type u} {s : Set α} : s ∉ {∅} ↔ s.Nonempty

@[deprecated Set.notMem_singleton_empty (since := "2025-05-24")]

theorem Set.nmem_singleton_empty {α : Type u} {s : Set α} : s ∉ {∅} ↔ s.Nonempty

Alias of Set.notMem_singleton_empty.

instance Set.uniqueSingleton {α : Type u} (a : α) : Unique ↑{a}

Equations

• Set.uniqueSingleton a = { default := ⟨a, ⋯⟩, uniq := ⋯ }

theorem Set.eq_singleton_iff_unique_mem {α : Type u} {s : Set α} {a : α} : s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a

theorem Set.eq_singleton_iff_nonempty_unique_mem {α : Type u} {s : Set α} {a : α} : s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a

theorem Set.setOf_mem_list_eq_replicate {α : Type u} {l : List α} {a : α} : {x : α | x ∈ l} = {a} ↔ ∃ n > 0, l = List.replicate n a

theorem Set.setOf_mem_list_eq_singleton_of_nodup {α : Type u} {l : List α} (H : l.Nodup) {a : α} : {x : α | x ∈ l} = {a} ↔ l = [a]

@[simp]

theorem Set.default_coe_singleton {α : Type u} (x : α) : default = ⟨x, ⋯⟩

@[simp]

theorem Set.subset_singleton_iff {α : Type u_1} {s : Set α} {x : α} : s ⊆ {x} ↔ ∀ y ∈ s, y = x

theorem Set.subset_singleton_iff_eq {α : Type u} {s : Set α} {x : α} : s ⊆ {x} ↔ s = ∅ ∨ s = {x}

theorem Set.Nonempty.subset_singleton_iff {α : Type u} {s : Set α} {a : α} (h : s.Nonempty) : s ⊆ {a} ↔ s = {a}

theorem Set.ssubset_singleton_iff {α : Type u} {s : Set α} {x : α} : s ⊂ {x} ↔ s = ∅

theorem Set.eq_empty_of_ssubset_singleton {α : Type u} {s : Set α} {x : α} (hs : s ⊂ {x}) : s = ∅

theorem Set.eq_of_nonempty_of_subsingleton {α : Type u_1} [Subsingleton α] (s t : Set α) [Nonempty ↑s] [Nonempty ↑t] : s = t

theorem Set.eq_of_nonempty_of_subsingleton' {α : Type u_1} [Subsingleton α] {s : Set α} (t : Set α) (hs : s.Nonempty) [Nonempty ↑t] : s = t

theorem Set.Nonempty.eq_zero {α : Type u} [Subsingleton α] [Zero α] {s : Set α} (h : s.Nonempty) : s = {0}

theorem Set.Nonempty.eq_one {α : Type u} [Subsingleton α] [One α] {s : Set α} (h : s.Nonempty) : s = {1}

Disjointness

@[simp]

theorem Set.disjoint_singleton_left {α : Type u} {s : Set α} {a : α} : Disjoint {a} s ↔ a ∉ s

@[simp]

theorem Set.disjoint_singleton_right {α : Type u} {s : Set α} {a : α} : Disjoint s {a} ↔ a ∉ s

theorem Set.disjoint_singleton {α : Type u} {a b : α} : Disjoint {a} {b} ↔ a ≠ b

theorem Set.ssubset_iff_sdiff_singleton {α : Type u} {s t : Set α} : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ {a}

@[simp]

theorem Set.disjoint_insert_left {α : Type u} {s t : Set α} {a : α} : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

@[simp]

theorem Set.disjoint_insert_right {α : Type u} {s t : Set α} {a : α} : Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t

Lemmas about complement

@[simp]

theorem Set.nonempty_compl_of_nontrivial {α : Type u} [Nontrivial α] (x : α) : {x}ᶜ.Nonempty

theorem Set.mem_compl_singleton_iff {α : Type u} {a x : α} : x ∈ {a}ᶜ ↔ x ≠ a

theorem Set.compl_singleton_eq {α : Type u} (a : α) : {a}ᶜ = {x : α | x ≠ a}

@[simp]

theorem Set.compl_ne_eq_singleton {α : Type u} (a : α) : {x : α | x ≠ a}ᶜ = {a}

@[simp]

theorem Set.subset_compl_singleton_iff {α : Type u} {a : α} {s : Set α} : s ⊆ {a}ᶜ ↔ a ∉ s

Lemmas about set difference

@[simp]

theorem Set.diff_singleton_subset_iff {α : Type u} {x : α} {s t : Set α} : s \ {x} ⊆ t ↔ s ⊆ insert x t

theorem Set.subset_diff_singleton {α : Type u} {x : α} {s t : Set α} (h : s ⊆ t) (hx : x ∉ s) : s ⊆ t \ {x}

theorem Set.subset_insert_diff_singleton {α : Type u} (x : α) (s : Set α) : s ⊆ insert x (s \ {x})

theorem Set.diff_insert_of_notMem {α : Type u} {s t : Set α} {x : α} (h : x ∉ s) : s \ insert x t = s \ t

@[deprecated Set.diff_insert_of_notMem (since := "2025-05-23")]

theorem Set.diff_insert_of_not_mem {α : Type u} {s t : Set α} {x : α} (h : x ∉ s) : s \ insert x t = s \ t

Alias of Set.diff_insert_of_notMem.

@[simp]

theorem Set.insert_diff_of_mem {α : Type u} {t : Set α} {a : α} (s : Set α) (h : a ∈ t) : insert a s \ t = s \ t

theorem Set.insert_diff_of_notMem {α : Type u} {t : Set α} {a : α} (s : Set α) (h : a ∉ t) : insert a s \ t = insert a (s \ t)

@[deprecated Set.insert_diff_of_notMem (since := "2025-05-23")]

theorem Set.insert_diff_of_not_mem {α : Type u} {t : Set α} {a : α} (s : Set α) (h : a ∉ t) : insert a s \ t = insert a (s \ t)

Alias of Set.insert_diff_of_notMem.

theorem Set.insert_diff_self_of_notMem {α : Type u} {a : α} {s : Set α} (h : a ∉ s) : insert a s \ {a} = s

@[deprecated Set.insert_diff_self_of_notMem (since := "2025-05-23")]

theorem Set.insert_diff_self_of_not_mem {α : Type u} {a : α} {s : Set α} (h : a ∉ s) : insert a s \ {a} = s

Alias of Set.insert_diff_self_of_notMem.

theorem Set.insert_diff_self_of_mem {α : Type u} {s : Set α} {a : α} (ha : a ∈ s) : insert a (s \ {a}) = s

theorem Set.insert_erase_invOn {α : Type u} {a : α} : InvOn (insert a) (fun (s : Set α) => s \ {a}) {s : Set α | a ∈ s} {s : Set α | a ∉ s}

theorem Set.insert_inj {α : Type u} {s : Set α} {a b : α} (ha : a ∉ s) : insert a s = insert b s ↔ a = b

@[simp]

theorem Set.insert_diff_eq_singleton {α : Type u} {a : α} {s : Set α} (h : a ∉ s) : insert a s \ s = {a}

theorem Set.inter_insert_of_mem {α : Type u} {s t : Set α} {a : α} (h : a ∈ s) : s ∩ insert a t = insert a (s ∩ t)

theorem Set.insert_inter_of_mem {α : Type u} {s t : Set α} {a : α} (h : a ∈ t) : insert a s ∩ t = insert a (s ∩ t)

theorem Set.inter_insert_of_notMem {α : Type u} {s t : Set α} {a : α} (h : a ∉ s) : s ∩ insert a t = s ∩ t

@[deprecated Set.inter_insert_of_notMem (since := "2025-05-23")]

theorem Set.inter_insert_of_not_mem {α : Type u} {s t : Set α} {a : α} (h : a ∉ s) : s ∩ insert a t = s ∩ t

Alias of Set.inter_insert_of_notMem.

theorem Set.insert_inter_of_notMem {α : Type u} {s t : Set α} {a : α} (h : a ∉ t) : insert a s ∩ t = s ∩ t

@[deprecated Set.insert_inter_of_notMem (since := "2025-05-23")]

theorem Set.insert_inter_of_not_mem {α : Type u} {s t : Set α} {a : α} (h : a ∉ t) : insert a s ∩ t = s ∩ t

Alias of Set.insert_inter_of_notMem.

@[simp]

theorem Set.diff_singleton_eq_self {α : Type u} {a : α} {s : Set α} (h : a ∉ s) : s \ {a} = s

theorem Set.diff_singleton_ssubset {α : Type u} {s : Set α} {a : α} : s \ {a} ⊂ s ↔ a ∈ s

@[deprecated Set.diff_singleton_ssubset (since := "2025-03-20")]

theorem Set.diff_singleton_sSubset {α : Type u} {s : Set α} {a : α} : s \ {a} ⊂ s ↔ a ∈ s

Alias of Set.diff_singleton_ssubset.

@[simp]

theorem Set.insert_diff_singleton {α : Type u} {a : α} {s : Set α} : insert a (s \ {a}) = insert a s

theorem Set.insert_diff_singleton_comm {α : Type u} {a b : α} (hab : a ≠ b) (s : Set α) : insert a (s \ {b}) = insert a s \ {b}

@[simp]

theorem Set.insert_diff_insert {α : Type u} {s t : Set α} {a : α} : insert a (s \ insert a t) = insert a (s \ t)

theorem Set.mem_diff_singleton {α : Type u} {x y : α} {s : Set α} : x ∈ s \ {y} ↔ x ∈ s ∧ x ≠ y

theorem Set.mem_diff_singleton_empty {α : Type u} {s : Set α} {t : Set (Set α)} : s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty

theorem Set.subset_insert_iff {α : Type u} {s t : Set α} {x : α} : s ⊆ insert x t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t

Lemmas about pairs

theorem Set.pair_eq_singleton {α : Type u} (a : α) : {a, a} = {a}

theorem Set.pair_comm {α : Type u} (a b : α) : {a, b} = {b, a}

theorem Set.pair_eq_pair_iff {α : Type u} {x y z w : α} : {x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z

theorem Set.pair_diff_left {α : Type u} {a b : α} (hne : a ≠ b) : {a, b} \ {a} = {b}

theorem Set.pair_diff_right {α : Type u} {a b : α} (hne : a ≠ b) : {a, b} \ {b} = {a}

theorem Set.pair_subset_iff {α : Type u} {s : Set α} {a b : α} : {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

theorem Set.pair_subset {α : Type u} {s : Set α} {a b : α} (ha : a ∈ s) (hb : b ∈ s) : {a, b} ⊆ s

theorem Set.subset_pair_iff {α : Type u} {s : Set α} {a b : α} : s ⊆ {a, b} ↔ ∀ x ∈ s, x = a ∨ x = b

theorem Set.subset_pair_iff_eq {α : Type u} {s : Set α} {x y : α} : s ⊆ {x, y} ↔ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

theorem Set.Nonempty.subset_pair_iff_eq {α : Type u} {s : Set α} {a b : α} (hs : s.Nonempty) : s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}

Powerset

theorem Set.powerset_singleton {α : Type u} (x : α) : 𝒫{x} = {∅, {x}}

The powerset of a singleton contains only ∅ and the singleton itself.

theorem Set.preimage_fst_singleton_eq_range {α : Type u_1} {β : Type u_2} {a : α} : Prod.fst ⁻¹' {a} = range fun (x : β) => (a, x)

theorem Set.preimage_snd_singleton_eq_range {α : Type u_1} {β : Type u_2} {b : β} : Prod.snd ⁻¹' {b} = range fun (x : α) => (x, b)

Lemmas about inclusion, the injection of subtypes induced by ⊆

Decidability instances for sets

instance Set.decidableSingleton {α : Type u} (a b : α) [Decidable (a = b)] : Decidable (a ∈ {b})

Equations

• Set.decidableSingleton a b = inferInstanceAs (Decidable (a = b))

@[simp]

theorem Prop.compl_singleton (p : Prop) : {p}ᶜ = {¬p}