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 a s is the set {a} ∪ s.

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

theorem Set.ne_insert_of_notMem {α : Type u_1} {s : Set α} (t : Set α) {a : α} : ¬a ∈ s → s ≠ insert a t

@[simp]

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

theorem Set.insert_ne_self {α : Type u_1} {s : Set α} {a : α} : insert a s ≠ s ↔ ¬a ∈ s

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

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

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

@[simp]

theorem Set.insert_subset_insert_iff {α : Type u_1} {s t : Set α} {a : α} (ha : ¬a ∈ s) : insert a s ⊆ insert a t ↔ s ⊆ t

theorem Set.subset_insert_iff_of_notMem {α : Type u_1} {s t : Set α} {a : α} (ha : ¬a ∈ s) : s ⊆ insert a t ↔ s ⊆ t

theorem Set.ssubset_iff_insert {α : Type u_1} {s t : Set α} : s ⊂ t ↔ ∃ (a : α), ¬a ∈ s ∧ insert a s ⊆ t

theorem LE.le.ssubset_of_mem_notMem {α : Type u_1} {s t : Set α} {a : α} (hst : s ⊆ t) (hat : a ∈ t) (has : ¬a ∈ s) : s ⊂ t

@[deprecated LE.le.ssubset_of_mem_notMem (since := "2026-06-05")]

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

Alias of LE.le.ssubset_of_mem_notMem.

theorem Set.ssubset_insert {α : Type u_1} {s : Set α} {a : α} (h : ¬a ∈ s) : s ⊂ insert a s

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

def Set.subtypeInsertEquivOption {α : Type u_1} [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_1} : LawfulSingleton α (Set α)

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

@[simp]

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

theorem Set.notMem_singleton_iff {α : Type u_1} {a b : α} : ¬a ∈ {b} ↔ a ≠ b

@[simp]

theorem Set.ofPred_eq_eq_singleton {α : Type u_1} {a : α} : {n : α | n = a} = {a}

@[deprecated Set.ofPred_eq_eq_singleton (since := "2026-07-09")]

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

Alias of Set.ofPred_eq_eq_singleton.

@[simp]

theorem Set.ofPred_eq_eq_singleton' {α : Type u_1} {a : α} : {x : α | a = x} = {a}

@[deprecated Set.ofPred_eq_eq_singleton' (since := "2026-07-09")]

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

Alias of Set.ofPred_eq_eq_singleton'.

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

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Set.empty_ne_singleton {α : Type u_1} (a : α) : ∅ ≠ {a}

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem Set.exists_mem_singleton {α : Type u_1} {P : α → Prop} {a : α} : (∃ (x : α), x ∈ {a} ∧ P x) ↔ P a

theorem Set.forall_mem_singleton {α : Type u_1} {P : α → Prop} {a : α} : (∀ (x : α), x ∈ {a} → P x) ↔ P a

@[simp]

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

@[simp]

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

@[simp]

theorem Set.singleton_inter_eq_empty {α : Type u_1} {s : Set α} {a : α} : {a} ∩ s = ∅ ↔ ¬a ∈ s

@[simp]

theorem Set.inter_singleton_eq_empty {α : Type u_1} {s : Set α} {a : α} : s ∩ {a} = ∅ ↔ ¬a ∈ s

@[simp]

theorem Set.singleton_inter_of_notMem {α : Type u_1} {s : Set α} {a : α} : ¬a ∈ s → {a} ∩ s = ∅

Alias of the reverse direction of Set.singleton_inter_eq_empty.

@[simp]

theorem Set.inter_singleton_of_notMem {α : Type u_1} {s : Set α} {a : α} : ¬a ∈ s → s ∩ {a} = ∅

Alias of the reverse direction of Set.inter_singleton_eq_empty.

@[simp]

theorem Set.singleton_inter_of_mem {α : Type u_1} {s : Set α} {a : α} (ha : a ∈ s) : {a} ∩ s = {a}

@[simp]

theorem Set.inter_singleton_of_mem {α : Type u_1} {s : Set α} {a : α} (ha : a ∈ s) : s ∩ {a} = {a}

theorem Set.notMem_singleton_empty {α : Type u_1} {s : Set α} : ¬s ∈ {∅} ↔ s.Nonempty

@[instance_reducible]

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

Equations

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

theorem Set.eq_singleton_iff_unique_mem {α : Type u_1} {s : Set α} {a : α} : s = {a} ↔ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a

theorem Set.eq_singleton_iff_nonempty_unique_mem {α : Type u_1} {s : Set α} {a : α} : s = {a} ↔ s.Nonempty ∧ ∀ (x : α), x ∈ s → x = a

theorem Set.singleton_iff_unique_mem {α : Type u_1} {s : Set α} : (∃ (a : α), s = {a}) ↔ ∃! a : α, a ∈ s

theorem Set.ofPred_mem_list_eq_replicate {α : Type u_1} {l : List α} {a : α} : {x : α | x ∈ l} = {a} ↔ ∃ (n : ℕ), n > 0 ∧ l = List.replicate n a

@[deprecated Set.ofPred_mem_list_eq_replicate (since := "2026-07-09")]

theorem Set.setOf_mem_list_eq_replicate {α : Type u_1} {l : List α} {a : α} : {x : α | x ∈ l} = {a} ↔ ∃ (n : ℕ), n > 0 ∧ l = List.replicate n a

Alias of Set.ofPred_mem_list_eq_replicate.

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

@[deprecated Set.ofPred_mem_list_eq_singleton_of_nodup (since := "2026-07-09")]

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

Alias of Set.ofPred_mem_list_eq_singleton_of_nodup.

@[simp]

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

@[simp]

theorem Set.subset_singleton_iff {α : Type u_3} {s : Set α} {x : α} : s ⊆ {x} ↔ ∀ (y : α), y ∈ s → y = x

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

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

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

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

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

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

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

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

Disjointness

@[simp]

theorem Set.disjoint_singleton_left {α : Type u_1} {s : Set α} {a : α} : Disjoint {a} s ↔ ¬a ∈ s

@[simp]

theorem Set.disjoint_singleton_right {α : Type u_1} {s : Set α} {a : α} : Disjoint s {a} ↔ ¬a ∈ s

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

@[simp]

theorem Set.disjoint_insert_left {α : Type u_1} {s t : Set α} {a : α} : Disjoint (insert a s) t ↔ ¬a ∈ t ∧ Disjoint s t

@[simp]

theorem Set.disjoint_insert_right {α : Type u_1} {s t : Set α} {a : α} : Disjoint s (insert a t) ↔ ¬a ∈ s ∧ Disjoint s t

theorem Set.insert_inj {α : Type u_1} {s : Set α} {a b : α} (ha : ¬a ∈ s) : insert a s = insert b s ↔ a = b

@[simp]

theorem Set.insert_sdiff_eq_singleton {α : Type u_1} {a : α} {s : Set α} (h : ¬a ∈ s) : insert a s \ s = {a}

@[deprecated Set.insert_sdiff_eq_singleton (since := "2026-06-03")]

theorem Set.insert_diff_eq_singleton {α : Type u_1} {a : α} {s : Set α} (h : ¬a ∈ s) : insert a s \ s = {a}

Alias of Set.insert_sdiff_eq_singleton.

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

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

theorem Set.inter_insert_of_notMem {α : Type u_1} {s t : Set α} {a : α} (h : ¬a ∈ s) : s ∩ insert a t = s ∩ t

theorem Set.insert_inter_of_notMem {α : Type u_1} {s t : Set α} {a : α} (h : ¬a ∈ t) : insert a s ∩ t = s ∩ t

Lemmas about pairs

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

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

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

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

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

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

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

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

theorem Set.range_ite_const {α : Type u_1} {β : Type u_2} {p : α → Prop} [DecidablePred p] {x y : β} (hp : ∃ (a : α), p a) (hn : ∃ (a : α), ¬p a) : (range fun (a : α) => if p a then x else y) = {x, y}

Powerset

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

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

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

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

Lemmas about inclusion, the injection of subtypes induced by ⊆

Decidability instances for sets

@[instance_reducible]

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

Equations

• Set.decidableSingleton a b = Set.decidableSingleton._aux_1 a b

@[simp]

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