doc-next-gen

Mathlib.Data.Set.Insert

Module docstring

{"# 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. ","### Lemmas about singletons ","### Disjointness ","### Lemmas about complement ","### Lemmas about set difference ","### Lemmas about pairs ","### Powerset ","### Lemmas about inclusion, the injection of subtypes induced by ⊆ ","### Decidability instances for sets "}

Set.insert_def theorem
(x : α) (s : Set α) : insert x s = {y | y = x ∨ y ∈ s}
Full source 
theorem insert_def (x : α) (s : Set α) : insert x s = { y | y = x ∨ y ∈ s } :=
  rfl
Definition of Set Insertion via Union with Singleton
Informal description
For any element $x$ of type $\alpha$ and any set $s$ of elements of type $\alpha$, the insertion of $x$ into $s$ is equal to the set $\{y \mid y = x \lor y \in s\}$.
Set.subset_insert theorem
(x : α) (s : Set α) : s ⊆ insert x s
Full source 
@[simp]
theorem subset_insert (x : α) (s : Set α) : s ⊆ insert x s := fun _ => Or.inr
Subset Property of Insertion: $s \subseteq \{x\} \cup s$
Informal description
For any element $x$ of type $\alpha$ and any set $s$ of elements of type $\alpha$, the set $s$ is a subset of the set obtained by inserting $x$ into $s$, i.e., $s \subseteq \{x\} \cup s$.
Set.mem_insert theorem
(x : α) (s : Set α) : x ∈ insert x s
Full source 
theorem mem_insert (x : α) (s : Set α) : x ∈ insert x s :=
  Or.inl rfl
Element Belongs to Its Insertion into Any Set
Informal description
For any element $x$ of type $\alpha$ and any set $s$ of elements of type $\alpha$, the element $x$ belongs to the set obtained by inserting $x$ into $s$, i.e., $x \in \{x\} \cup s$.
Set.mem_insert_of_mem theorem
{x : α} {s : Set α} (y : α) : x ∈ s → x ∈ insert y s
Full source 
theorem mem_insert_of_mem {x : α} {s : Set α} (y : α) : x ∈ s → x ∈ insert y s :=
  Or.inr
Membership Preservation Under Insertion
Informal description
For any element $x$ in a set $s$ over a type $\alpha$, and for any element $y$ of $\alpha$, $x$ is also in the set obtained by inserting $y$ into $s$.
Set.mem_of_mem_insert_of_ne theorem
: b ∈ insert a s → b ≠ a → b ∈ s
Full source 
theorem mem_of_mem_insert_of_ne : b ∈ insert a s → b ≠ a → b ∈ s :=
  Or.resolve_left
Membership in Inserted Set with Non-Equality Implies Membership in Original Set
Informal description
For any elements $a, b$ of a type $\alpha$ and any set $s$ of elements of $\alpha$, if $b$ belongs to the set $\{a\} \cup s$ and $b \neq a$, then $b$ must belong to $s$.
Set.mem_insert_iff theorem
{x a : α} {s : Set α} : x ∈ insert a s ↔ x = a ∨ x ∈ s
Full source 
@[simp]
theorem mem_insert_iff {x a : α} {s : Set α} : x ∈ insert a sx ∈ insert a s ↔ x = a ∨ x ∈ s :=
  Iff.rfl
Membership in Inserted Set: $x \in \{a\} \cup s \leftrightarrow x = a \lor x \in s$
Informal description
For any element $x$ and set $s$ of type $\alpha$, and for any element $a$ of type $\alpha$, the statement $x \in \{a\} \cup s$ holds if and only if either $x = a$ or $x \in s$.
Set.insert_eq_of_mem theorem
{a : α} {s : Set α} (h : a ∈ s) : insert a s = s
Full source 
@[simp]
theorem insert_eq_of_mem {a : α} {s : Set α} (h : a ∈ s) : insert a s = s :=
  ext fun _ => or_iff_right_of_imp fun e => e.symm ▸ h
Insertion of Existing Element Leaves Set Unchanged
Informal description
For any element $a$ in a set $s$ over a type $\alpha$, the insertion of $a$ into $s$ results in the same set $s$, i.e., $\{a\} \cup s = s$.
Set.ne_insert_of_not_mem theorem
{s : Set α} (t : Set α) {a : α} : a ∉ s → s ≠ insert a t
Full source 
theorem ne_insert_of_not_mem {s : Set α} (t : Set α) {a : α} : a ∉ s → s ≠ insert a t :=
  mt fun e => e.symm ▸ mem_insert _ _
Non-membership Implies Inequality After Insertion: $a \notin s \implies s \neq \{a\} \cup t$
Informal description
For any set $s$ and $t$ over a type $\alpha$, and any element $a \in \alpha$, if $a$ does not belong to $s$, then $s$ is not equal to the set obtained by inserting $a$ into $t$, i.e., $a \notin s \implies s \neq \{a\} \cup t$.
Set.insert_ne_self theorem
: insert a s ≠ s ↔ a ∉ s
Full source 
theorem insert_ne_self : insertinsert a s ≠ sinsert a s ≠ s ↔ a ∉ s :=
  insert_eq_self.not
Insertion Alters Set if and only if Element is New: $\{a\} \cup s \neq s \leftrightarrow a \notin s$
Informal description
For any element $a$ of type $\alpha$ and any set $s$ of elements of type $\alpha$, the insertion of $a$ into $s$ is not equal to $s$ if and only if $a$ is not an element of $s$, i.e., $\{a\} \cup s \neq s \leftrightarrow a \notin s$.
Set.insert_subset_iff theorem
: insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
Full source 
theorem insert_subset_iff : insertinsert a s ⊆ tinsert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by
  simp only [subset_def, mem_insert_iff, or_imp, forall_and, forall_eq]
Subset Condition for Insertion: $\{a\} \cup s \subseteq t \leftrightarrow a \in t \land s \subseteq t$
Informal description
For any element $a$ of type $\alpha$ and sets $s, t$ over $\alpha$, the set $\{a\} \cup s$ is a subset of $t$ if and only if $a$ is an element of $t$ and $s$ is a subset of $t$.
Set.insert_subset theorem
(ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t
Full source 
theorem insert_subset (ha : a ∈ t) (hs : s ⊆ t) : insertinsert a s ⊆ t :=
  insert_subset_iff.mpr ⟨ha, hs⟩
Insertion Preserves Subset Property: $\{a\} \cup s \subseteq t$ when $a \in t$ and $s \subseteq t$
Informal description
For any element $a$ in a set $t$ and any subset $s \subseteq t$, the set $\{a\} \cup s$ is a subset of $t$.
Set.insert_subset_insert theorem
(h : s ⊆ t) : insert a s ⊆ insert a t
Full source 
theorem insert_subset_insert (h : s ⊆ t) : insertinsert a s ⊆ insert a t := fun _ => Or.imp_right (@h _)
Insertion Preserves Subset Relation: $\{a\} \cup s \subseteq \{a\} \cup t$ when $s \subseteq t$
Informal description
For any element $a$ and sets $s, t$ of type $\alpha$, if $s \subseteq t$, then $\{a\} \cup s \subseteq \{a\} \cup t$.
Set.insert_subset_insert_iff theorem
(ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t
Full source 
@[simp] theorem insert_subset_insert_iff (ha : a ∉ s) : insertinsert a s ⊆ insert a tinsert a s ⊆ insert a t ↔ s ⊆ t := by
  refine ⟨fun h x hx => ?_, insert_subset_insert⟩
  rcases h (subset_insert _ _ hx) with (rfl | hxt)
  exacts [(ha hx).elim, hxt]
Insertion Preserves Subset Relation if and only if Original Sets Satisfy Subset Relation (for Non-Member Element)
Informal description
For any element $a$ and sets $s, t$ of type $\alpha$, if $a \notin s$, then $\{a\} \cup s \subseteq \{a\} \cup t$ if and only if $s \subseteq t$.
Set.subset_insert_iff_of_not_mem theorem
(ha : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t
Full source 
theorem subset_insert_iff_of_not_mem (ha : a ∉ s) : s ⊆ insert a ts ⊆ insert a t ↔ s ⊆ t :=
  forall₂_congr fun _ hb => or_iff_right <| ne_of_mem_of_not_mem hb ha
Subset Relation with Insertion of Non-Member Element: $s \subseteq \{a\} \cup t \leftrightarrow s \subseteq t$ when $a \notin s$
Informal description
For any element $a$ and sets $s, t$ of type $\alpha$, if $a \notin s$, then $s \subseteq \{a\} \cup t$ if and only if $s \subseteq t$.
Set.ssubset_iff_insert theorem
{s t : Set α} : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t
Full source 
theorem ssubset_iff_insert {s t : Set α} : s ⊂ ts ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t := by
  simp only [insert_subset_iff, exists_and_right, ssubset_def, not_subset]
  aesop
Characterization of Strict Subset via Insertion: $s \subset t \leftrightarrow \exists a \notin s, \{a\} \cup s \subseteq t$
Informal description
For any sets $s$ and $t$ of type $\alpha$, $s$ is a strict subset of $t$ if and only if there exists an element $a \notin s$ such that $\{a\} \cup s \subseteq t$.
HasSubset.Subset.ssubset_of_mem_not_mem theorem
(hst : s ⊆ t) (hat : a ∈ t) (has : a ∉ s) : s ⊂ t
Full source 
theorem _root_.HasSubset.Subset.ssubset_of_mem_not_mem (hst : s ⊆ t) (hat : a ∈ t) (has : a ∉ s) :
    s ⊂ t := hst.ssubset_of_not_subset fun a ↦ has (a hat)
Strict Subset Condition via Non-Membership: $s \subset t$ when $s \subseteq t$ and $\exists a \in t \setminus s$
Informal description
For any sets $s$ and $t$ of type $\alpha$, if $s \subseteq t$ and there exists an element $a \in t$ such that $a \notin s$, then $s$ is a strict subset of $t$, i.e., $s \subset t$.
Set.ssubset_insert theorem
{s : Set α} {a : α} (h : a ∉ s) : s ⊂ insert a s
Full source 
theorem ssubset_insert {s : Set α} {a : α} (h : a ∉ s) : s ⊂ insert a s :=
  ssubset_iff_insert.2 ⟨a, h, Subset.rfl⟩
Strict Subset Property of Insertion: $s \subset \{a\} \cup s$ for $a \notin s$
Informal description
For any set $s$ of elements of type $\alpha$ and any element $a \notin s$, the set $s$ is a strict subset of the set obtained by inserting $a$ into $s$, i.e., $s \subset \{a\} \cup s$.
Set.insert_comm theorem
(a b : α) (s : Set α) : insert a (insert b s) = insert b (insert a s)
Full source 
theorem insert_comm (a b : α) (s : Set α) : insert a (insert b s) = insert b (insert a s) :=
  ext fun _ => or_left_comm
Commutativity of Insertion in Sets: $\{a\} \cup (\{b\} \cup s) = \{b\} \cup (\{a\} \cup s)$
Informal description
For any elements $a, b$ of a type $\alpha$ and any set $s$ of elements of $\alpha$, the set obtained by inserting $a$ into the set resulting from inserting $b$ into $s$ is equal to the set obtained by inserting $b$ into the set resulting from inserting $a$ into $s$. In other words, $\{a\} \cup (\{b\} \cup s) = \{b\} \cup (\{a\} \cup s)$.
Set.insert_idem theorem
(a : α) (s : Set α) : insert a (insert a s) = insert a s
Full source 
theorem insert_idem (a : α) (s : Set α) : insert a (insert a s) = insert a s :=
  insert_eq_of_mem <| mem_insert _ _
Idempotence of Set Insertion: $\{a\} \cup (\{a\} \cup s) = \{a\} \cup s$
Informal description
For any element $a$ of type $\alpha$ and any set $s$ over $\alpha$, inserting $a$ into the set obtained by inserting $a$ into $s$ results in the same set as simply inserting $a$ into $s$, i.e., $\{a\} \cup (\{a\} \cup s) = \{a\} \cup s$.
Set.insert_union theorem
: insert a s ∪ t = insert a (s ∪ t)
Full source 
theorem insert_union : insertinsert a s ∪ t = insert a (s ∪ t) :=
  ext fun _ => or_assoc
Union with Insertion: $\{a\} \cup s \cup t = \{a\} \cup (s \cup t)$
Informal description
For any element $a$ of type $\alpha$ and sets $s, t$ over $\alpha$, the union of the set $\{a\} \cup s$ with $t$ is equal to the set $\{a\} \cup (s \cup t)$. In symbols: $$ \{a\} \cup s \cup t = \{a\} \cup (s \cup t) $$
Set.union_insert theorem
: s ∪ insert a t = insert a (s ∪ t)
Full source 
@[simp]
theorem union_insert : s ∪ insert a t = insert a (s ∪ t) :=
  ext fun _ => or_left_comm
Union with Insertion Equals Insertion of Union
Informal description
For any set $s$ and any element $a$ in a type $\alpha$, and any set $t$ of elements of $\alpha$, the union of $s$ with the insertion of $a$ into $t$ is equal to the insertion of $a$ into the union of $s$ and $t$. In symbols: $$ s \cup (\{a\} \cup t) = \{a\} \cup (s \cup t) $$
Set.insert_nonempty theorem
(a : α) (s : Set α) : (insert a s).Nonempty
Full source 
@[simp]
theorem insert_nonempty (a : α) (s : Set α) : (insert a s).Nonempty :=
  ⟨a, mem_insert a s⟩
Nonemptyness of Insertion: $\{a\} \cup s$ is nonempty
Informal description
For any element $a$ of type $\alpha$ and any set $s$ over $\alpha$, the set $\{a\} \cup s$ is nonempty.
Set.instNonemptyElemInsert instance
(a : α) (s : Set α) : Nonempty (insert a s : Set α)
Full source 
instance (a : α) (s : Set α) : Nonempty (insert a s : Set α) :=
  (insert_nonempty a s).to_subtype
Nonemptyness of Insertion into Sets
Informal description
For any element $a$ of type $\alpha$ and any set $s$ over $\alpha$, the set $\{a\} \cup s$ is nonempty.
Set.insert_inter_distrib theorem
(a : α) (s t : Set α) : insert a (s ∩ t) = insert a s ∩ insert a t
Full source 
theorem insert_inter_distrib (a : α) (s t : Set α) : insert a (s ∩ t) = insertinsert a s ∩ insert a t :=
  ext fun _ => or_and_left
Distributivity of Insertion over Intersection: $\{a\} \cup (s \cap t) = (\{a\} \cup s) \cap (\{a\} \cup t)$
Informal description
For any element $a$ of type $\alpha$ and any sets $s, t$ over $\alpha$, the insertion of $a$ into the intersection $s \cap t$ is equal to the intersection of the insertions of $a$ into $s$ and $a$ into $t$. That is, $\{a\} \cup (s \cap t) = (\{a\} \cup s) \cap (\{a\} \cup t)$.
Set.insert_union_distrib theorem
(a : α) (s t : Set α) : insert a (s ∪ t) = insert a s ∪ insert a t
Full source 
theorem insert_union_distrib (a : α) (s t : Set α) : insert a (s ∪ t) = insertinsert a s ∪ insert a t :=
  ext fun _ => or_or_distrib_left
Distributivity of Insertion over Union: $\{a\} \cup (s \cup t) = (\{a\} \cup s) \cup (\{a\} \cup t)$
Informal description
For any element $a$ of type $\alpha$ and any sets $s, t$ over $\alpha$, the insertion of $a$ into the union $s \cup t$ is equal to the union of the insertions of $a$ into $s$ and $a$ into $t$. That is, $\{a\} \cup (s \cup t) = (\{a\} \cup s) \cup (\{a\} \cup t)$.
Set.forall_of_forall_insert theorem
{P : α → Prop} {a : α} {s : Set α} (H : ∀ x, x ∈ insert a s → P x) (x) (h : x ∈ s) : P x
Full source 
theorem forall_of_forall_insert {P : α → Prop} {a : α} {s : Set α} (H : ∀ x, x ∈ insert a s → P x)
    (x) (h : x ∈ s) : P x :=
  H _ (Or.inr h)
Universal Property of Insertion: From $\forall x \in \{a\} \cup s, P(x)$ to $\forall x \in s, P(x)$
Informal description
For any predicate $P$ on elements of type $\alpha$, any element $a \in \alpha$, and any set $s \subseteq \alpha$, if $P(x)$ holds for all $x$ in the set $\{a\} \cup s$, then for any particular $x \in s$, $P(x)$ holds.
Set.forall_insert_of_forall theorem
{P : α → Prop} {a : α} {s : Set α} (H : ∀ x, x ∈ s → P x) (ha : P a) (x) (h : x ∈ insert a s) : P x
Full source 
theorem forall_insert_of_forall {P : α → Prop} {a : α} {s : Set α} (H : ∀ x, x ∈ s → P x) (ha : P a)
    (x) (h : x ∈ insert a s) : P x :=
  h.elim (fun e => e.symm ▸ ha) (H _)
Universal Property of Insertion: If $P$ holds on $s$ and $a$, then it holds on $\{a\} \cup s$
Informal description
For any predicate $P$ on elements of a type $\alpha$, if $P$ holds for all elements in a set $s \subseteq \alpha$ and also holds for a particular element $a \in \alpha$, then $P$ holds for all elements in the set $\{a\} \cup s$.
Set.exists_mem_insert theorem
{P : α → Prop} {a : α} {s : Set α} : (∃ x ∈ insert a s, P x) ↔ (P a ∨ ∃ x ∈ s, P x)
Full source 
theorem exists_mem_insert {P : α → Prop} {a : α} {s : Set α} :
    (∃ x ∈ insert a s, P x) ↔ (P a ∨ ∃ x ∈ s, P x) := by
  simp [mem_insert_iff, or_and_right, exists_and_left, exists_or]
Existence in Union with Singleton: $(\exists x \in \{a\} \cup s, P(x)) \leftrightarrow P(a) \lor (\exists x \in s, P(x))$
Informal description
For any predicate $P$ on elements of a type $\alpha$, an element $a \in \alpha$, and a set $s \subseteq \alpha$, there exists an element $x$ in the set $\{a\} \cup s$ satisfying $P(x)$ if and only if either $P(a)$ holds or there exists an element $x \in s$ satisfying $P(x)$. In symbols: $$(\exists x \in \{a\} \cup s, P(x)) \leftrightarrow (P(a) \lor (\exists x \in s, P(x)))$$
Set.forall_mem_insert theorem
{P : α → Prop} {a : α} {s : Set α} : (∀ x ∈ insert a s, P x) ↔ P a ∧ ∀ x ∈ s, P x
Full source 
theorem forall_mem_insert {P : α → Prop} {a : α} {s : Set α} :
    (∀ x ∈ insert a s, P x) ↔ P a ∧ ∀ x ∈ s, P x :=
  forall₂_or_left.trans <| and_congr_left' forall_eq
Universal Quantifier over Inserted Set Equals Conjunction of Predicate at Point and Rest of Set
Informal description
For any predicate $P$ on elements of a type $\alpha$, any element $a \in \alpha$, and any set $s \subseteq \alpha$, the following are equivalent: 1. For all $x$ in the set $\{a\} \cup s$, the predicate $P(x)$ holds. 2. Both $P(a)$ holds and for all $x \in s$, $P(x)$ holds. In symbols: $$(\forall x \in \{a\} \cup s, P(x)) \leftrightarrow P(a) \land (\forall x \in s, P(x))$$
Set.subtypeInsertEquivOption definition
[DecidableEq α] {t : Set α} {x : α} (h : x ∉ t) : { i // i ∈ insert x t } ≃ Option { i // i ∈ t }
Full source 
/-- Inserting an element to a set is equivalent to the option type. -/
def subtypeInsertEquivOption
    [DecidableEq α] {t : Set α} {x : α} (h : x ∉ t) :
    { i // i ∈ insert x t }{ i // i ∈ insert x t } ≃ Option { i // i ∈ t } where
  toFun y := if h : ↑y = x then none else some ⟨y, (mem_insert_iff.mp y.2).resolve_left h⟩
  invFun y := (y.elim ⟨x, mem_insert _ _⟩) fun z => ⟨z, mem_insert_of_mem _ z.2⟩
  left_inv y := by
    by_cases h : ↑y = x
    · simp only [Subtype.ext_iff, h, Option.elim, dif_pos, Subtype.coe_mk]
    · simp only [h, Option.elim, dif_neg, not_false_iff, Subtype.coe_eta, Subtype.coe_mk]
  right_inv := by
    rintro (_ | y)
    · simp only [Option.elim, dif_pos]
    · have : ↑y ≠ x := by
        rintro ⟨⟩
        exact h y.2
      simp only [this, Option.elim, Subtype.eta, dif_neg, not_false_iff, Subtype.coe_mk]
Equivalence between inserted set subtype and option type
Informal description
For a type $\alpha$ with decidable equality, given a set $t \subseteq \alpha$ and an element $x \notin t$, the subtype $\{i \mid i \in \{x\} \cup t\}$ is equivalent to the option type $\text{Option } \{i \mid i \in t\}$. More precisely, there exists a bijection between: 1. The set of elements in $\{x\} \cup t$ (viewed as a subtype), and 2. The option type where: - $\text{none}$ corresponds to $x$, and - $\text{some } y$ corresponds to an element $y \in t$.
Set.singleton_def theorem
(a : α) : ({ a } : Set α) = insert a ∅
Full source 
theorem singleton_def (a : α) : ({a} : Set α) = insert a ∅ :=
  (insert_empty_eq a).symm
Singleton Set as Insertion into Empty Set: $\{a\} = \text{insert } a \emptyset$
Informal description
For any element $a$ of a type $\alpha$, the singleton set $\{a\}$ is equal to the insertion of $a$ into the empty set, i.e., $\{a\} = \text{insert } a \emptyset$.
Set.mem_singleton_iff theorem
{a b : α} : a ∈ ({ b } : Set α) ↔ a = b
Full source 
@[simp]
theorem mem_singleton_iff {a b : α} : a ∈ ({b} : Set α)a ∈ ({b} : Set α) ↔ a = b :=
  Iff.rfl
Membership in Singleton Set is Equivalent to Equality: $a \in \{b\} \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ of a type $\alpha$, the element $a$ belongs to the singleton set $\{b\}$ if and only if $a = b$.
Set.not_mem_singleton_iff theorem
{a b : α} : a ∉ ({ b } : Set α) ↔ a ≠ b
Full source 
theorem not_mem_singleton_iff {a b : α} : a ∉ ({b} : Set α)a ∉ ({b} : Set α) ↔ a ≠ b :=
  Iff.rfl
Non-membership in Singleton Set is Equivalent to Inequality: $a \notin \{b\} \leftrightarrow a \neq b$
Informal description
For any elements $a$ and $b$ of a type $\alpha$, the statement $a \notin \{b\}$ is equivalent to $a \neq b$.
Set.setOf_eq_eq_singleton theorem
{a : α} : {n | n = a} = { a }
Full source 
@[simp]
theorem setOf_eq_eq_singleton {a : α} : { n | n = a } = {a} :=
  rfl
Set Comprehension of Equality Yields Singleton: $\{n \mid n = a\} = \{a\}$
Informal description
For any element $a$ of type $\alpha$, the set $\{n \mid n = a\}$ is equal to the singleton set $\{a\}$.
Set.setOf_eq_eq_singleton' theorem
{a : α} : {x | a = x} = { a }
Full source 
@[simp]
theorem setOf_eq_eq_singleton' {a : α} : { x | a = x } = {a} :=
  ext fun _ => eq_comm
Set Comprehension of Equality Yields Singleton: $\{x \mid a = x\} = \{a\}$
Informal description
For any element $a$ of type $\alpha$, the set $\{x \mid a = x\}$ is equal to the singleton set $\{a\}$.
Set.mem_singleton theorem
(a : α) : a ∈ ({ a } : Set α)
Full source 
theorem mem_singleton (a : α) : a ∈ ({a} : Set α) :=
  @rfl _ _
Element Belongs to Its Singleton Set: $a \in \{a\}$
Informal description
For any element $a$ of type $\alpha$, the element $a$ belongs to the singleton set $\{a\}$.
Set.singleton_eq_singleton_iff theorem
{x y : α} : { x } = ({ y } : Set α) ↔ x = y
Full source 
@[simp]
theorem singleton_eq_singleton_iff {x y : α} : {x}{x} = ({y} : Set α) ↔ x = y :=
  Set.ext_iff.trans eq_iff_eq_cancel_left
Equality of Singleton Sets: $\{x\} = \{y\} \leftrightarrow x = y$
Informal description
For any elements $x$ and $y$ of a type $\alpha$, the singleton sets $\{x\}$ and $\{y\}$ are equal if and only if $x = y$.
Set.singleton_injective theorem
: Injective (singleton : α → Set α)
Full source 
theorem singleton_injective : Injective (singleton : α → Set α) := fun _ _ =>
  singleton_eq_singleton_iff.mp
Injectivity of the Singleton Set Construction
Informal description
The singleton set function $\{ \cdot \} : \alpha \to \text{Set } \alpha$ is injective. That is, for any elements $x, y \in \alpha$, if $\{x\} = \{y\}$, then $x = y$.
Set.mem_singleton_of_eq theorem
{x y : α} (H : x = y) : x ∈ ({ y } : Set α)
Full source 
theorem mem_singleton_of_eq {x y : α} (H : x = y) : x ∈ ({y} : Set α) :=
  H
Membership in Singleton Set via Equality
Informal description
For any elements $x$ and $y$ of a type $\alpha$, if $x = y$, then $x$ belongs to the singleton set $\{y\}$.
Set.insert_eq theorem
(x : α) (s : Set α) : insert x s = ({ x } : Set α) ∪ s
Full source 
theorem insert_eq (x : α) (s : Set α) : insert x s = ({x} : Set α) ∪ s :=
  rfl
Insertion as Union with Singleton: $\text{insert}(x, s) = \{x\} \cup s$
Informal description
For any element $x$ of a type $\alpha$ and any set $s$ of elements of $\alpha$, the insertion of $x$ into $s$ is equal to the union of the singleton set $\{x\}$ and $s$, i.e., $\text{insert}(x, s) = \{x\} \cup s$.
Set.singleton_nonempty theorem
(a : α) : ({ a } : Set α).Nonempty
Full source 
@[simp]
theorem singleton_nonempty (a : α) : ({a} : Set α).Nonempty :=
  ⟨a, rfl⟩
Nonemptiness of Singleton Sets
Informal description
For any element $a$ of a type $\alpha$, the singleton set $\{a\}$ is nonempty.
Set.singleton_ne_empty theorem
(a : α) : ({ a } : Set α) ≠ ∅
Full source 
@[simp]
theorem singleton_ne_empty (a : α) : ({a} : Set α) ≠ ∅ :=
  (singleton_nonempty _).ne_empty
Non-emptiness of Singleton Sets: $\{a\} \neq \emptyset$
Informal description
For any element $a$ of a type $\alpha$, the singleton set $\{a\}$ is not equal to the empty set $\emptyset$.
Set.singleton_subset_iff theorem
{a : α} {s : Set α} : { a } ⊆ s ↔ a ∈ s
Full source 
@[simp]
theorem singleton_subset_iff {a : α} {s : Set α} : {a}{a} ⊆ s{a} ⊆ s ↔ a ∈ s :=
  forall_eq
Singleton Subset Criterion: $\{a\} \subseteq s \leftrightarrow a \in s$
Informal description
For any element $a$ of type $\alpha$ and any set $s$ over $\alpha$, the singleton set $\{a\}$ is a subset of $s$ if and only if $a$ is an element of $s$.
Set.singleton_subset_singleton theorem
: ({ a } : Set α) ⊆ { b } ↔ a = b
Full source 
theorem singleton_subset_singleton : ({a} : Set α) ⊆ {b}({a} : Set α) ⊆ {b} ↔ a = b := by simp
Singleton Subset Condition: $\{a\} \subseteq \{b\} \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ of type $\alpha$, the singleton set $\{a\}$ is a subset of the singleton set $\{b\}$ if and only if $a = b$.
Set.set_compr_eq_eq_singleton theorem
{a : α} : {b | b = a} = { a }
Full source 
theorem set_compr_eq_eq_singleton {a : α} : { b | b = a } = {a} :=
  rfl
Set Comprehension Equals Singleton: $\{b \mid b = a\} = \{a\}$
Informal description
For any element $a$ of type $\alpha$, the set $\{b \mid b = a\}$ is equal to the singleton set $\{a\}$.
Set.singleton_union theorem
: { a } ∪ s = insert a s
Full source 
@[simp]
theorem singleton_union : {a}{a} ∪ s = insert a s :=
  rfl
Union of Singleton with Set Equals Insertion: $\{a\} \cup s = \text{insert } a \text{ } s$
Informal description
For any element $a$ of type $\alpha$ and any set $s$ over $\alpha$, the union of the singleton set $\{a\}$ with $s$ is equal to the insertion of $a$ into $s$, i.e., $\{a\} \cup s = \text{insert } a \text{ } s$.
Set.union_singleton theorem
: s ∪ { a } = insert a s
Full source 
@[simp]
theorem union_singleton : s ∪ {a} = insert a s :=
  union_comm _ _
Union with Singleton Equals Insertion: $s \cup \{a\} = \text{insert } a \text{ } s$
Informal description
For any set $s$ over a type $\alpha$ and any element $a \in \alpha$, the union of $s$ with the singleton set $\{a\}$ is equal to the insertion of $a$ into $s$, i.e., $s \cup \{a\} = \text{insert } a \text{ } s$.
Set.singleton_inter_eq_empty theorem
: { a } ∩ s = ∅ ↔ a ∉ s
Full source 
@[simp]
theorem singleton_inter_eq_empty : {a}{a} ∩ s{a} ∩ s = ∅ ↔ a ∉ s :=
  not_nonempty_iff_eq_empty.symm.trans singleton_inter_nonempty.not
Empty Intersection of Singleton and Set is Equivalent to Non-membership
Informal description
For any element $a$ of type $\alpha$ and any set $s$ over $\alpha$, the intersection of the singleton set $\{a\}$ with $s$ is empty if and only if $a$ does not belong to $s$, i.e., $\{a\} \cap s = \emptyset \leftrightarrow a \notin s$.
Set.inter_singleton_eq_empty theorem
: s ∩ { a } = ∅ ↔ a ∉ s
Full source 
@[simp]
theorem inter_singleton_eq_empty : s ∩ {a}s ∩ {a} = ∅ ↔ a ∉ s := by
  rw [inter_comm, singleton_inter_eq_empty]
Empty Intersection of Set and Singleton: $s \cap \{a\} = \emptyset \leftrightarrow a \notin s$
Informal description
For any set $s$ over a type $\alpha$ and any element $a \in \alpha$, the intersection $s \cap \{a\}$ is empty if and only if $a$ does not belong to $s$, i.e., $s \cap \{a\} = \emptyset \leftrightarrow a \notin s$.
Set.nmem_singleton_empty theorem
{s : Set α} : s ∉ ({∅} : Set (Set α)) ↔ s.Nonempty
Full source 
theorem nmem_singleton_empty {s : Set α} : s ∉ ({∅} : Set (Set α))s ∉ ({∅} : Set (Set α)) ↔ s.Nonempty :=
  nonempty_iff_ne_empty.symm
Nonempty Set Characterization via Singleton Empty Set: $s \notin \{\emptyset\} \leftrightarrow s \neq \emptyset$
Informal description
For any set $s$ over a type $\alpha$, the statement $s \notin \{\emptyset\}$ holds if and only if $s$ is nonempty, i.e., $s \neq \emptyset$.
Set.setOf_mem_list_eq_replicate theorem
{l : List α} {a : α} : {x | x ∈ l} = { a } ↔ ∃ n > 0, l = List.replicate n a
Full source 
theorem setOf_mem_list_eq_replicate {l : List α} {a : α} :
    { x | x ∈ l }{ x | x ∈ l } = {a} ↔ ∃ n > 0, l = List.replicate n a := by
  simpa +contextual [Set.ext_iff, iff_iff_implies_and_implies, forall_and, List.eq_replicate_iff,
    List.length_pos_iff_exists_mem] using ⟨fun _ _ ↦ ⟨_, ‹_›⟩, fun x hx h ↦ h _ hx ▸ hx⟩
Characterization of Singleton Set from List Membership via Replication
Informal description
For a list $l$ of elements of type $\alpha$ and an element $a \in \alpha$, the set $\{x \mid x \in l\}$ is equal to the singleton set $\{a\}$ if and only if there exists a positive integer $n$ such that $l$ is a list consisting of $n$ copies of $a$, i.e., $l = \text{replicate}\,n\,a$.
Set.setOf_mem_list_eq_singleton_of_nodup theorem
{l : List α} (H : l.Nodup) {a : α} : {x | x ∈ l} = { a } ↔ l = [a]
Full source 
theorem setOf_mem_list_eq_singleton_of_nodup {l : List α} (H : l.Nodup) {a : α} :
    { x | x ∈ l }{ x | x ∈ l } = {a} ↔ l = [a] := by
  constructor
  · rw [setOf_mem_list_eq_replicate]
    rintro ⟨n, hn, rfl⟩
    simp only [List.nodup_replicate] at H
    simp [show n = 1 by omega]
  · rintro rfl
    simp
Characterization of Singleton Set from Distinct List Membership
Informal description
For a list $l$ of distinct elements of type $\alpha$ (i.e., $l$ has no duplicates) and an element $a \in \alpha$, the set $\{x \mid x \in l\}$ is equal to the singleton set $\{a\}$ if and only if $l$ is the list containing exactly $a$, i.e., $l = [a]$.
Set.default_coe_singleton theorem
(x : α) : (default : ({ x } : Set α)) = ⟨x, rfl⟩
Full source 
@[simp]
theorem default_coe_singleton (x : α) : (default : ({x} : Set α)) = ⟨x, rfl⟩ :=
  rfl
Default Element of Singleton Set is Its Sole Member
Informal description
For any element $x$ of a type $\alpha$, the default element of the singleton set $\{x\}$ is the element $x$ itself, paired with a proof that $x \in \{x\}$ (which is trivial by reflexivity).
Set.subset_singleton_iff theorem
{α : Type*} {s : Set α} {x : α} : s ⊆ { x } ↔ ∀ y ∈ s, y = x
Full source 
@[simp]
theorem subset_singleton_iff {α : Type*} {s : Set α} {x : α} : s ⊆ {x}s ⊆ {x} ↔ ∀ y ∈ s, y = x :=
  Iff.rfl
Characterization of Subset of Singleton Set: $s \subseteq \{x\} \leftrightarrow \forall y \in s, y = x$
Informal description
For any set $s$ and element $x$ of type $\alpha$, the set $s$ is a subset of the singleton $\{x\}$ if and only if every element $y$ in $s$ is equal to $x$.
Set.subset_singleton_iff_eq theorem
{s : Set α} {x : α} : s ⊆ { x } ↔ s = ∅ ∨ s = { x }
Full source 
theorem subset_singleton_iff_eq {s : Set α} {x : α} : s ⊆ {x}s ⊆ {x} ↔ s = ∅ ∨ s = {x} := by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · exact ⟨fun _ => Or.inl rfl, fun _ => empty_subset _⟩
  · simp [eq_singleton_iff_nonempty_unique_mem, hs, hs.ne_empty]
Subset of Singleton Characterization: $s \subseteq \{x\} \leftrightarrow s = \emptyset \lor s = \{x\}$
Informal description
For any set $s$ and element $x$ of type $\alpha$, the set $s$ is a subset of the singleton $\{x\}$ if and only if $s$ is either the empty set or the singleton $\{x\}$ itself.
Set.Nonempty.subset_singleton_iff theorem
(h : s.Nonempty) : s ⊆ { a } ↔ s = { a }
Full source 
theorem Nonempty.subset_singleton_iff (h : s.Nonempty) : s ⊆ {a}s ⊆ {a} ↔ s = {a} :=
  subset_singleton_iff_eq.trans <| or_iff_right h.ne_empty
Characterization of Nonempty Subset of Singleton Set: $s \subseteq \{a\} \leftrightarrow s = \{a\}$
Informal description
For any nonempty set $s$ over a type $\alpha$ and any element $a \in \alpha$, the set $s$ is a subset of the singleton $\{a\}$ if and only if $s$ is equal to $\{a\}$.
Set.ssubset_singleton_iff theorem
{s : Set α} {x : α} : s ⊂ { x } ↔ s = ∅
Full source 
theorem ssubset_singleton_iff {s : Set α} {x : α} : s ⊂ {x}s ⊂ {x} ↔ s = ∅ := by
  rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false,
    and_iff_left_iff_imp]
  exact fun h => h ▸ (singleton_ne_empty _).symm
Strict Subset of Singleton Characterization: $s \subset \{x\} \leftrightarrow s = \emptyset$
Informal description
For any set $s$ and element $x$ of type $\alpha$, the strict subset relation $s \subset \{x\}$ holds if and only if $s$ is the empty set.
Set.disjoint_singleton_left theorem
: Disjoint { a } s ↔ a ∉ s
Full source 
@[simp default+1]
lemma disjoint_singleton_left : DisjointDisjoint {a} s ↔ a ∉ s := by simp [Set.disjoint_iff, subset_def]
Disjointness of Singleton and Set: $\{a\} \cap s = \emptyset \leftrightarrow a \notin s$
Informal description
For any element $a$ of type $\alpha$ and any set $s$ over $\alpha$, the singleton set $\{a\}$ is disjoint from $s$ if and only if $a$ does not belong to $s$, i.e., $\{a\} \cap s = \emptyset \leftrightarrow a \notin s$.
Set.disjoint_singleton_right theorem
: Disjoint s { a } ↔ a ∉ s
Full source 
@[simp]
lemma disjoint_singleton_right : DisjointDisjoint s {a} ↔ a ∉ s :=
  disjoint_comm.trans disjoint_singleton_left
Disjointness of Set and Singleton: $s \cap \{a\} = \emptyset \leftrightarrow a \notin s$
Informal description
For any set $s$ and any element $a$ of type $\alpha$, the set $s$ is disjoint from the singleton set $\{a\}$ if and only if $a$ does not belong to $s$, i.e., $s \cap \{a\} = \emptyset \leftrightarrow a \notin s$.
Set.disjoint_singleton theorem
: Disjoint ({ a } : Set α) { b } ↔ a ≠ b
Full source 
lemma disjoint_singleton : DisjointDisjoint ({a} : Set α) {b} ↔ a ≠ b := by
  simp
Disjointness of Singletons: $\{a\} \cap \{b\} = \emptyset \iff a \neq b$
Informal description
For any elements $a$ and $b$ in a type $\alpha$, the singleton sets $\{a\}$ and $\{b\}$ are disjoint if and only if $a \neq b$.
Set.ssubset_iff_sdiff_singleton theorem
: s ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ { a }
Full source 
lemma ssubset_iff_sdiff_singleton : s ⊂ ts ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ {a} := by
  simp [ssubset_iff_insert, subset_diff, insert_subset_iff]; aesop
Strict Subset Characterization via Singleton Removal: $s \subset t \iff \exists a \in t, s \subseteq t \setminus \{a\}$
Informal description
For any sets $s$ and $t$ over a type $\alpha$, $s$ is a strict subset of $t$ if and only if there exists an element $a \in t$ such that $s$ is a subset of $t$ with $a$ removed, i.e., $s \subseteq t \setminus \{a\}$.
Set.disjoint_insert_left theorem
: Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t
Full source 
@[simp]
theorem disjoint_insert_left : DisjointDisjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t := by
  simp only [Set.disjoint_left, Set.mem_insert_iff, forall_eq_or_imp]
Disjointness Condition for Insertion on the Left
Informal description
For any element $a$ and sets $s, t$ in a type $\alpha$, the set $\{a\} \cup s$ is disjoint from $t$ if and only if $a$ does not belong to $t$ and $s$ is disjoint from $t$. In symbols: $$ \{a\} \cup s \cap t = \emptyset \ \Leftrightarrow \ a \notin t \ \text{and} \ s \cap t = \emptyset. $$
Set.disjoint_insert_right theorem
: Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t
Full source 
@[simp]
theorem disjoint_insert_right : DisjointDisjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t := by
  rw [disjoint_comm, disjoint_insert_left, disjoint_comm]
Disjointness Condition for Insertion on the Right
Informal description
For any element $a$ and sets $s, t$ in a type $\alpha$, the set $s$ is disjoint from $\{a\} \cup t$ if and only if $a$ does not belong to $s$ and $s$ is disjoint from $t$. In symbols: $$ s \cap (\{a\} \cup t) = \emptyset \ \Leftrightarrow \ a \notin s \ \text{and} \ s \cap t = \emptyset. $$
Set.nonempty_compl_of_nontrivial theorem
[Nontrivial α] (x : α) : Set.Nonempty { x }ᶜ
Full source 
@[simp] lemma nonempty_compl_of_nontrivial [Nontrivial α] (x : α) : Set.Nonempty {x}{x}ᶜ := by
  obtain ⟨y, hy⟩ := exists_ne x
  exact ⟨y, by simp [hy]⟩
Nonempty Complement of Singleton in Nontrivial Types
Informal description
For any nontrivial type $\alpha$ and any element $x \in \alpha$, the complement of the singleton set $\{x\}$ is nonempty.
Set.mem_compl_singleton_iff theorem
{a x : α} : x ∈ ({ a } : Set α)ᶜ ↔ x ≠ a
Full source 
theorem mem_compl_singleton_iff {a x : α} : x ∈ ({a} : Set α)ᶜx ∈ ({a} : Set α)ᶜ ↔ x ≠ a :=
  Iff.rfl
Characterization of Complement of Singleton Set: $x \in \{a\}^c \leftrightarrow x \neq a$
Informal description
For any elements $a$ and $x$ of a type $\alpha$, the element $x$ belongs to the complement of the singleton set $\{a\}$ if and only if $x$ is not equal to $a$, i.e., $x \in \{a\}^c \leftrightarrow x \neq a$.
Set.compl_singleton_eq theorem
(a : α) : ({ a } : Set α)ᶜ = {x | x ≠ a}
Full source 
theorem compl_singleton_eq (a : α) : ({a} : Set α)ᶜ = { x | x ≠ a } :=
  rfl
Complement of Singleton Set Equals Set of Non-Equal Elements
Informal description
For any element $a$ of a type $\alpha$, the complement of the singleton set $\{a\}$ is equal to the set of all elements $x$ in $\alpha$ such that $x \neq a$, i.e., $\{a\}^c = \{x \mid x \neq a\}$.
Set.compl_ne_eq_singleton theorem
(a : α) : ({x | x ≠ a} : Set α)ᶜ = { a }
Full source 
@[simp]
theorem compl_ne_eq_singleton (a : α) : ({ x | x ≠ a } : Set α)ᶜ = {a} :=
  compl_compl _
Complement of Set of Non-Equal Elements is Singleton
Informal description
For any element $a$ of a type $\alpha$, the complement of the set $\{x \mid x \neq a\}$ is equal to the singleton set $\{a\}$, i.e., $\{x \mid x \neq a\}^c = \{a\}$.
Set.subset_compl_singleton_iff theorem
{a : α} {s : Set α} : s ⊆ { a }ᶜ ↔ a ∉ s
Full source 
@[simp]
theorem subset_compl_singleton_iff {a : α} {s : Set α} : s ⊆ {a}ᶜs ⊆ {a}ᶜ ↔ a ∉ s :=
  subset_compl_comm.trans singleton_subset_iff
Subset of Singleton Complement Criterion: $s \subseteq \{a\}^c \leftrightarrow a \notin s$
Informal description
For any element $a$ of a type $\alpha$ and any set $s$ over $\alpha$, the set $s$ is a subset of the complement of the singleton $\{a\}$ if and only if $a$ is not an element of $s$. In symbols: $$ s \subseteq \{a\}^c \leftrightarrow a \notin s. $$
Set.diff_singleton_subset_iff theorem
{x : α} {s t : Set α} : s \ { x } ⊆ t ↔ s ⊆ insert x t
Full source 
@[simp]
theorem diff_singleton_subset_iff {x : α} {s t : Set α} : s \ {x}s \ {x} ⊆ ts \ {x} ⊆ t ↔ s ⊆ insert x t := by
  rw [← union_singleton, union_comm]
  apply diff_subset_iff
Characterization of Set Difference via Singleton Insertion: $s \setminus \{x\} \subseteq t \leftrightarrow s \subseteq \{x\} \cup t$
Informal description
For any element $x$ of a type $\alpha$ and any sets $s, t$ over $\alpha$, the set difference $s \setminus \{x\}$ is a subset of $t$ if and only if $s$ is a subset of the insertion of $x$ into $t$. In symbols: $$ s \setminus \{x\} \subseteq t \leftrightarrow s \subseteq \{x\} \cup t $$
Set.subset_diff_singleton theorem
{x : α} {s t : Set α} (h : s ⊆ t) (hx : x ∉ s) : s ⊆ t \ { x }
Full source 
theorem subset_diff_singleton {x : α} {s t : Set α} (h : s ⊆ t) (hx : x ∉ s) : s ⊆ t \ {x} :=
  subset_inter h <| subset_compl_comm.1 <| singleton_subset_iff.2 hx
Subset Preservation under Set Difference with Non-Member Singleton: $s \subseteq t \land x \notin s \to s \subseteq t \setminus \{x\}$
Informal description
For any element $x$ of a type $\alpha$ and any sets $s, t$ over $\alpha$, if $s$ is a subset of $t$ and $x$ does not belong to $s$, then $s$ is a subset of the set difference $t \setminus \{x\}$.
Set.subset_insert_diff_singleton theorem
(x : α) (s : Set α) : s ⊆ insert x (s \ { x })
Full source 
theorem subset_insert_diff_singleton (x : α) (s : Set α) : s ⊆ insert x (s \ {x}) := by
  rw [← diff_singleton_subset_iff]
Set Inclusion via Insertion and Difference: $s \subseteq \{x\} \cup (s \setminus \{x\})$
Informal description
For any element $x$ of a type $\alpha$ and any set $s$ over $\alpha$, the set $s$ is a subset of the insertion of $x$ into the set difference $s \setminus \{x\}$. In symbols: $$ s \subseteq \{x\} \cup (s \setminus \{x\}) $$
Set.diff_insert_of_not_mem theorem
{x : α} (h : x ∉ s) : s \ insert x t = s \ t
Full source 
theorem diff_insert_of_not_mem {x : α} (h : x ∉ s) : s \ insert x t = s \ t := by
  refine Subset.antisymm (diff_subset_diff (refl _) (subset_insert ..)) fun y hy ↦ ?_
  simp only [mem_diff, mem_insert_iff, not_or] at hy ⊢
  exact ⟨hy.1, fun hxy ↦ h <| hxy ▸ hy.1, hy.2⟩
Set Difference with Insertion of Non-Member Element: $s \setminus (\{x\} \cup t) = s \setminus t$ when $x \notin s$
Informal description
For any element $x$ and sets $s, t$ over a type $\alpha$, if $x \notin s$, then the set difference $s \setminus (\{x\} \cup t)$ is equal to $s \setminus t$.
Set.insert_diff_of_mem theorem
(s) (h : a ∈ t) : insert a s \ t = s \ t
Full source 
@[simp]
theorem insert_diff_of_mem (s) (h : a ∈ t) : insertinsert a s \ t = s \ t := by
  ext
  constructor <;> simp +contextual [or_imp, h]
Set Difference with Insertion of an Element Already in the Second Set
Informal description
For any element $a$ and sets $s$ and $t$ over a type $\alpha$, if $a \in t$, then the set difference between $\{a\} \cup s$ and $t$ is equal to the set difference between $s$ and $t$, i.e., $(\{a\} \cup s) \setminus t = s \setminus t$.
Set.insert_diff_of_not_mem theorem
(s) (h : a ∉ t) : insert a s \ t = insert a (s \ t)
Full source 
theorem insert_diff_of_not_mem (s) (h : a ∉ t) : insertinsert a s \ t = insert a (s \ t) := by
  classical
    ext x
    by_cases h' : x ∈ t
    · simp [h, h', ne_of_mem_of_not_mem h' h]
    · simp [h, h']
Insertion and Set Difference for Non-Member Elements: $\{a\} \cup s \setminus t = \{a\} \cup (s \setminus t)$ when $a \notin t$
Informal description
For any element $a$ not in set $t$, and for any set $s$, the set difference between $\{a\} \cup s$ and $t$ is equal to $\{a\} \cup (s \setminus t)$.
Set.insert_diff_self_of_not_mem theorem
{a : α} {s : Set α} (h : a ∉ s) : insert a s \ { a } = s
Full source 
theorem insert_diff_self_of_not_mem {a : α} {s : Set α} (h : a ∉ s) : insertinsert a s \ {a} = s := by
  ext x
  simp [and_iff_left_of_imp (ne_of_mem_of_not_mem · h)]
Set difference of insertion with non-member singleton: $(\{a\} \cup s) \setminus \{a\} = s$ when $a \notin s$
Informal description
For any element $a$ and set $s$ over a type $\alpha$, if $a \notin s$, then the set difference between $\{a\} \cup s$ and $\{a\}$ is equal to $s$, i.e., $(\{a\} \cup s) \setminus \{a\} = s$.
Set.insert_diff_self_of_mem theorem
(ha : a ∈ s) : insert a (s \ { a }) = s
Full source 
lemma insert_diff_self_of_mem (ha : a ∈ s) : insert a (s \ {a}) = s := by
  ext; simp +contextual [or_and_left, em, ha]
Insertion of Element into Its Own Difference Yields Original Set
Informal description
For any element $a$ in a set $s$, the insertion of $a$ into the set difference $s \setminus \{a\}$ equals $s$, i.e., $\{a\} \cup (s \setminus \{a\}) = s$.
Set.insert_erase_invOn theorem
: InvOn (insert a) (fun s ↦ s \ { a }) {s : Set α | a ∈ s} {s : Set α | a ∉ s}
Full source 
lemma insert_erase_invOn :
    InvOn (insert a) (fun s ↦ s \ {a}) {s : Set α | a ∈ s} {s : Set α | a ∉ s} :=
  ⟨fun _s ha ↦ insert_diff_self_of_mem ha, fun _s ↦ insert_diff_self_of_not_mem⟩
Inverse Relationship Between Insertion and Removal of an Element in Sets
Informal description
The function that inserts an element $a$ into a set and the function that removes $a$ from a set (via set difference) are mutual inverses when restricted to appropriate domains. Specifically: 1. For any set $s$ containing $a$, removing $a$ and then reinserting it returns $s$. 2. For any set $s$ not containing $a$, inserting $a$ and then removing it returns $s$. In other words, the pair $(insert\ a, s \mapsto s \setminus \{a\})$ forms an inverse relationship between: - The collection of sets containing $a$ - The collection of sets not containing $a$
Set.insert_inj theorem
(ha : a ∉ s) : insert a s = insert b s ↔ a = b
Full source 
theorem insert_inj (ha : a ∉ s) : insertinsert a s = insert b s ↔ a = b :=
  ⟨fun h => eq_of_not_mem_of_mem_insert (h ▸ mem_insert a s) ha,
    congr_arg (fun x => insert x s)⟩
Injection Property of Insertion: $\{a\} \cup s = \{b\} \cup s \leftrightarrow a = b$ when $a \notin s$
Informal description
For any element $a$ not in a set $s$, the equality $\{a\} \cup s = \{b\} \cup s$ holds if and only if $a = b$.
Set.insert_diff_eq_singleton theorem
{a : α} {s : Set α} (h : a ∉ s) : insert a s \ s = { a }
Full source 
@[simp]
theorem insert_diff_eq_singleton {a : α} {s : Set α} (h : a ∉ s) : insertinsert a s \ s = {a} := by
  ext
  rw [Set.mem_diff, Set.mem_insert_iff, Set.mem_singleton_iff, or_and_right, and_not_self_iff,
    or_false, and_iff_left_iff_imp]
  rintro rfl
  exact h
Set Difference of Inserted Element Equals Singleton: $(\{a\} \cup s) \setminus s = \{a\}$ when $a \notin s$
Informal description
For any element $a$ of type $\alpha$ and any set $s$ of type $\alpha$, if $a$ is not in $s$, then the set difference between $\{a\} \cup s$ and $s$ is the singleton set $\{a\}$. In symbols: \[ (\{a\} \cup s) \setminus s = \{a\}. \]
Set.inter_insert_of_mem theorem
(h : a ∈ s) : s ∩ insert a t = insert a (s ∩ t)
Full source 
theorem inter_insert_of_mem (h : a ∈ s) : s ∩ insert a t = insert a (s ∩ t) := by
  rw [insert_inter_distrib, insert_eq_of_mem h]
Intersection with Insertion of Member Element
Informal description
For any element $a$ in a set $s$ (i.e., $a \in s$), the intersection of $s$ with the set obtained by inserting $a$ into another set $t$ is equal to the insertion of $a$ into the intersection of $s$ and $t$. In symbols: $$ s \cap (\{a\} \cup t) = \{a\} \cup (s \cap t) $$
Set.insert_inter_of_mem theorem
(h : a ∈ t) : insert a s ∩ t = insert a (s ∩ t)
Full source 
theorem insert_inter_of_mem (h : a ∈ t) : insertinsert a s ∩ t = insert a (s ∩ t) := by
  rw [insert_inter_distrib, insert_eq_of_mem h]
Intersection with Insertion of Member Element: $\{a\} \cup s \cap t = \{a\} \cup (s \cap t)$ when $a \in t$
Informal description
For any element $a$ in a set $t$ and any set $s$ over a type $\alpha$, the intersection of the set obtained by inserting $a$ into $s$ with $t$ is equal to the set obtained by inserting $a$ into the intersection of $s$ and $t$. In symbols: \[ \{a\} \cup s \cap t = \{a\} \cup (s \cap t) \quad \text{if} \quad a \in t. \]
Set.inter_insert_of_not_mem theorem
(h : a ∉ s) : s ∩ insert a t = s ∩ t
Full source 
theorem inter_insert_of_not_mem (h : a ∉ s) : s ∩ insert a t = s ∩ t :=
  ext fun _ => and_congr_right fun hx => or_iff_right <| ne_of_mem_of_not_mem hx h
Intersection with Insertion of Non-Member Element
Informal description
For any element $a$ not in a set $s$ (i.e., $a \notin s$), the intersection of $s$ with the set obtained by inserting $a$ into another set $t$ is equal to the intersection of $s$ with $t$ itself. In symbols: $$ s \cap (\{a\} \cup t) = s \cap t $$
Set.insert_inter_of_not_mem theorem
(h : a ∉ t) : insert a s ∩ t = s ∩ t
Full source 
theorem insert_inter_of_not_mem (h : a ∉ t) : insertinsert a s ∩ t = s ∩ t :=
  ext fun _ => and_congr_left fun hx => or_iff_right <| ne_of_mem_of_not_mem hx h
Intersection with Insertion of Non-Member Element
Informal description
For any element $a$ not in a set $t$, and for any sets $s$ and $t$ over a type $\alpha$, the intersection of the set obtained by inserting $a$ into $s$ with $t$ is equal to the intersection of $s$ with $t$. In symbols: \[ \{a\} \cup s \cap t = s \cap t \quad \text{if} \quad a \notin t. \]
Set.diff_singleton_eq_self theorem
{a : α} {s : Set α} (h : a ∉ s) : s \ { a } = s
Full source 
@[simp]
theorem diff_singleton_eq_self {a : α} {s : Set α} (h : a ∉ s) : s \ {a} = s :=
  sdiff_eq_self_iff_disjoint.2 <| by simp [h]
Set Difference with Singleton of Non-Member Element Preserves Set
Informal description
For any element $a$ not in a set $s$, the set difference $s \setminus \{a\}$ is equal to $s$ itself.
Set.diff_singleton_ssubset theorem
{s : Set α} {a : α} : s \ { a } ⊂ s ↔ a ∈ s
Full source 
theorem diff_singleton_ssubset {s : Set α} {a : α} : s \ {a}s \ {a} ⊂ ss \ {a} ⊂ s ↔ a ∈ s := by
  simp
Strict Subset Condition for Set Difference with Singleton
Informal description
For any set $s$ over a type $\alpha$ and any element $a \in \alpha$, the set difference $s \setminus \{a\}$ is a strict subset of $s$ if and only if $a$ belongs to $s$. In symbols: \[ s \setminus \{a\} \subset s \leftrightarrow a \in s. \]
Set.insert_diff_singleton theorem
{a : α} {s : Set α} : insert a (s \ { a }) = insert a s
Full source 
@[simp]
theorem insert_diff_singleton {a : α} {s : Set α} : insert a (s \ {a}) = insert a s := by
  simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]
Insertion-Difference Identity: $\{a\} \cup (s \setminus \{a\}) = \{a\} \cup s$
Informal description
For any element $a$ of type $\alpha$ and any set $s$ over $\alpha$, the insertion of $a$ into the set difference $s \setminus \{a\}$ equals the insertion of $a$ into $s$, i.e., $\{a\} \cup (s \setminus \{a\}) = \{a\} \cup s$.
Set.insert_diff_singleton_comm theorem
(hab : a ≠ b) (s : Set α) : insert a (s \ { b }) = insert a s \ { b }
Full source 
theorem insert_diff_singleton_comm (hab : a ≠ b) (s : Set α) :
    insert a (s \ {b}) = insertinsert a s \ {b} := by
  simp_rw [← union_singleton, union_diff_distrib,
    diff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)]
Commutativity of Insertion and Set Difference with Singleton: $\{a\} \cup (s \setminus \{b\}) = (\{a\} \cup s) \setminus \{b\}$ for $a \neq b$
Informal description
For any distinct elements $a$ and $b$ of a type $\alpha$ and any set $s$ over $\alpha$, the insertion of $a$ into the set difference $s \setminus \{b\}$ is equal to the set difference of the insertion of $a$ into $s$ and the singleton $\{b\}$. In symbols: $$\{a\} \cup (s \setminus \{b\}) = (\{a\} \cup s) \setminus \{b\}.$$
Set.insert_diff_insert theorem
: insert a (s \ insert a t) = insert a (s \ t)
Full source 
@[simp]
theorem insert_diff_insert : insert a (s \ insert a t) = insert a (s \ t) := by
  rw [← union_singleton (s := t), ← diff_diff, insert_diff_singleton]
Insertion-Difference Identity: $\{a\} \cup (s \setminus (\{a\} \cup t)) = \{a\} \cup (s \setminus t)$
Informal description
For any element $a$ of a type $\alpha$ and any sets $s, t$ over $\alpha$, the insertion of $a$ into the set difference $s \setminus (\{a\} \cup t)$ equals the insertion of $a$ into the set difference $s \setminus t$. In symbols: $$\{a\} \cup (s \setminus (\{a\} \cup t)) = \{a\} \cup (s \setminus t).$$
Set.mem_diff_singleton theorem
{x y : α} {s : Set α} : x ∈ s \ { y } ↔ x ∈ s ∧ x ≠ y
Full source 
theorem mem_diff_singleton {x y : α} {s : Set α} : x ∈ s \ {y}x ∈ s \ {y} ↔ x ∈ s ∧ x ≠ y :=
  Iff.rfl
Characterization of Set Difference with Singleton: $x \in s \setminus \{y\} \leftrightarrow x \in s \land x \neq y$
Informal description
For any elements $x, y$ of a type $\alpha$ and any set $s$ over $\alpha$, the element $x$ belongs to the set difference $s \setminus \{y\}$ if and only if $x$ belongs to $s$ and $x$ is not equal to $y$. In symbols: $$x \in s \setminus \{y\} \leftrightarrow x \in s \land x \neq y.$$
Set.mem_diff_singleton_empty theorem
{t : Set (Set α)} : s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty
Full source 
theorem mem_diff_singleton_empty {t : Set (Set α)} : s ∈ t \ {∅}s ∈ t \ {∅} ↔ s ∈ t ∧ s.Nonempty :=
  mem_diff_singleton.trans <| and_congr_right' nonempty_iff_ne_empty.symm
Characterization of Nonempty Sets in a Collection: $s \in t \setminus \{\emptyset\} \leftrightarrow s \in t \land s \neq \emptyset$
Informal description
For any set $s$ in a collection of sets $t$ over a type $\alpha$, the set $s$ belongs to the difference $t \setminus \{\emptyset\}$ if and only if $s$ belongs to $t$ and $s$ is nonempty. In symbols: $$s \in t \setminus \{\emptyset\} \leftrightarrow s \in t \land s \neq \emptyset.$$
Set.subset_insert_iff theorem
{s t : Set α} {x : α} : s ⊆ insert x t ↔ s ⊆ t ∨ (x ∈ s ∧ s \ { x } ⊆ t)
Full source 
theorem subset_insert_iff {s t : Set α} {x : α} :
    s ⊆ insert x ts ⊆ insert x t ↔ s ⊆ t ∨ (x ∈ s ∧ s \ {x} ⊆ t) := by
  rw [← diff_singleton_subset_iff]
  by_cases hx : x ∈ s
  · rw [and_iff_right hx, or_iff_right_of_imp diff_subset.trans]
  rw [diff_singleton_eq_self hx, or_iff_left_of_imp And.right]
Characterization of Subset via Insertion: $s \subseteq \{x\} \cup t \leftrightarrow s \subseteq t \lor (x \in s \land s \setminus \{x\} \subseteq t)$
Informal description
For any sets $s, t$ over a type $\alpha$ and any element $x \in \alpha$, the subset relation $s \subseteq \{x\} \cup t$ holds if and only if either $s \subseteq t$ or ($x \in s$ and $s \setminus \{x\} \subseteq t$).
Set.pair_eq_singleton theorem
(a : α) : ({ a, a } : Set α) = { a }
Full source 
theorem pair_eq_singleton (a : α) : ({a, a} : Set α) = {a} :=
  union_self _
Pair Set of Identical Elements Equals Singleton Set
Informal description
For any element $a$ of a type $\alpha$, the pair set $\{a, a\}$ is equal to the singleton set $\{a\}$.
Set.pair_comm theorem
(a b : α) : ({ a, b } : Set α) = { b, a }
Full source 
theorem pair_comm (a b : α) : ({a, b} : Set α) = {b, a} :=
  union_comm _ _
Commutativity of Pair Sets: $\{a, b\} = \{b, a\}$
Informal description
For any two elements $a$ and $b$ of a type $\alpha$, the pair set $\{a, b\}$ is equal to the pair set $\{b, a\}$.
Set.pair_eq_pair_iff theorem
{x y z w : α} : ({ x, y } : Set α) = { z, w } ↔ x = z ∧ y = w ∨ x = w ∧ y = z
Full source 
theorem pair_eq_pair_iff {x y z w : α} :
    ({x, y} : Set α) = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z := by
  simp [subset_antisymm_iff, insert_subset_iff]; aesop
Equality of Pair Sets: $\{x, y\} = \{z, w\}$ iff $x=z \land y=w$ or $x=w \land y=z$
Informal description
For any elements $x, y, z, w$ of a type $\alpha$, the pair set $\{x, y\}$ is equal to the pair set $\{z, w\}$ if and only if either ($x = z$ and $y = w$) or ($x = w$ and $y = z$).
Set.pair_diff_left theorem
(hne : a ≠ b) : ({ a, b } : Set α) \ { a } = { b }
Full source 
theorem pair_diff_left (hne : a ≠ b) : ({a, b} : Set α) \ {a} = {b} := by
  rw [insert_diff_of_mem _ (mem_singleton a), diff_singleton_eq_self (by simpa)]
Left Difference of Pair Set with Singleton: $\{a, b\} \setminus \{a\} = \{b\}$ for $a \neq b$
Informal description
For any two distinct elements $a$ and $b$ of a type $\alpha$, the set difference between the pair set $\{a, b\}$ and the singleton $\{a\}$ equals the singleton $\{b\}$, i.e., $\{a, b\} \setminus \{a\} = \{b\}$.
Set.pair_diff_right theorem
(hne : a ≠ b) : ({ a, b } : Set α) \ { b } = { a }
Full source 
theorem pair_diff_right (hne : a ≠ b) : ({a, b} : Set α) \ {b} = {a} := by
  rw [pair_comm, pair_diff_left hne.symm]
Right Difference of Pair Set with Singleton: $\{a, b\} \setminus \{b\} = \{a\}$ for $a \neq b$
Informal description
For any two distinct elements $a$ and $b$ of a type $\alpha$, the set difference between the pair set $\{a, b\}$ and the singleton $\{b\}$ equals the singleton $\{a\}$, i.e., $\{a, b\} \setminus \{b\} = \{a\}$.
Set.pair_subset theorem
(ha : a ∈ s) (hb : b ∈ s) : { a, b } ⊆ s
Full source 
theorem pair_subset (ha : a ∈ s) (hb : b ∈ s) : {a, b}{a, b} ⊆ s :=
  pair_subset_iff.2 ⟨ha,hb⟩
Pair Set Subset Property: $\{a, b\} \subseteq s$ when $a, b \in s$
Informal description
For any elements $a$ and $b$ in a set $s$ over a type $\alpha$, the pair set $\{a, b\}$ is a subset of $s$.
Set.subset_pair_iff theorem
: s ⊆ { a, b } ↔ ∀ x ∈ s, x = a ∨ x = b
Full source 
theorem subset_pair_iff : s ⊆ {a, b}s ⊆ {a, b} ↔ ∀ x ∈ s, x = a ∨ x = b := by
  simp [subset_def]
Characterization of Subset of a Pair: $s \subseteq \{a, b\} \leftrightarrow \forall x \in s, x = a \lor x = b$
Informal description
For any set $s$ and elements $a, b$ of type $\alpha$, the subset relation $s \subseteq \{a, b\}$ holds if and only if every element $x \in s$ satisfies $x = a$ or $x = b$.
Set.subset_pair_iff_eq theorem
{x y : α} : s ⊆ { x, y } ↔ s = ∅ ∨ s = { x } ∨ s = { y } ∨ s = { x, y }
Full source 
theorem subset_pair_iff_eq {x y : α} : s ⊆ {x, y}s ⊆ {x, y} ↔ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y} := by
  refine ⟨?_, by rintro (rfl | rfl | rfl | rfl) <;> simp [pair_subset_iff]⟩
  rw [subset_insert_iff, subset_singleton_iff_eq, subset_singleton_iff_eq,
    ← subset_empty_iff (s := s \ {x}), diff_subset_iff, union_empty, subset_singleton_iff_eq]
  have h : x ∈ s → {y} = s \ {x} → s = {x,y} := fun h₁ h₂ ↦ by simp [h₁, h₂]
  tauto
Characterization of Subsets of a Pair: $s \subseteq \{x, y\} \leftrightarrow s \in \{\emptyset, \{x\}, \{y\}, \{x, y\}\}$
Informal description
For any set $s$ and elements $x, y$ of type $\alpha$, the subset relation $s \subseteq \{x, y\}$ holds if and only if $s$ is either the empty set, the singleton $\{x\}$, the singleton $\{y\}$, or the pair $\{x, y\}$.
Set.Nonempty.subset_pair_iff_eq theorem
(hs : s.Nonempty) : s ⊆ { a, b } ↔ s = { a } ∨ s = { b } ∨ s = { a, b }
Full source 
theorem Nonempty.subset_pair_iff_eq (hs : s.Nonempty) :
    s ⊆ {a, b}s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b} := by
  rw [Set.subset_pair_iff_eq, or_iff_right]; exact hs.ne_empty
Characterization of Nonempty Subsets of a Pair: $s \subseteq \{a, b\} \leftrightarrow s \in \{\{a\}, \{b\}, \{a, b\}\}$
Informal description
For any nonempty set $s$ and elements $a, b$ of type $\alpha$, the subset relation $s \subseteq \{a, b\}$ holds if and only if $s$ is either the singleton $\{a\}$, the singleton $\{b\}$, or the pair $\{a, b\}$.
Set.powerset_singleton theorem
(x : α) : 𝒫({ x } : Set α) = {∅, { x }}
Full source 
/-- The powerset of a singleton contains only `∅` and the singleton itself. -/
theorem powerset_singleton (x : α) : 𝒫({x} : Set α) = {∅, {x}} := by
  ext y
  rw [mem_powerset_iff, subset_singleton_iff_eq, mem_insert_iff, mem_singleton_iff]
Powerset of a Singleton: $\mathcal{P}(\{x\}) = \{\emptyset, \{x\}\}$
Informal description
For any element $x$ of a type $\alpha$, the powerset of the singleton set $\{x\}$ consists of exactly two sets: the empty set $\emptyset$ and the singleton set $\{x\}$ itself. In other words, $\mathcal{P}(\{x\}) = \{\emptyset, \{x\}\}$.
Set.preimage_fst_singleton_eq_range theorem
: (Prod.fst ⁻¹' { a } : Set (α × β)) = range (a, ·)
Full source 
lemma preimage_fst_singleton_eq_range : (Prod.fstProd.fst ⁻¹' {a} : Set (α × β)) = range (a, ·) := by
  aesop
Preimage of Singleton under First Projection Equals Range of Pairing Function
Informal description
For any elements $a \in \alpha$ and $b \in \beta$, the preimage of the singleton set $\{a\}$ under the first projection $\mathrm{fst} : \alpha \times \beta \to \alpha$ is equal to the range of the function $\lambda b \mapsto (a, b)$. In other words, $$ \mathrm{fst}^{-1}(\{a\}) = \{(a, b) \mid b \in \beta\}. $$
Set.preimage_snd_singleton_eq_range theorem
: (Prod.snd ⁻¹' { b } : Set (α × β)) = range (·, b)
Full source 
lemma preimage_snd_singleton_eq_range : (Prod.sndProd.snd ⁻¹' {b} : Set (α × β)) = range (·, b) := by
  aesop
Preimage of Singleton under Second Projection Equals Range of Pairing Function
Informal description
For any elements $a \in \alpha$ and $b \in \beta$, the preimage of the singleton set $\{b\}$ under the second projection $\mathrm{snd} : \alpha \times \beta \to \beta$ is equal to the range of the function $\lambda a \mapsto (a, b)$. In other words, $$ \mathrm{snd}^{-1}(\{b\}) = \{(a, b) \mid a \in \alpha\}. $$
Set.decidableSingleton instance
[Decidable (a = b)] : Decidable (a ∈ ({ b } : Set α))
Full source 
instance decidableSingleton [Decidable (a = b)] : Decidable (a ∈ ({b} : Set α)) :=
  inferInstanceAs (Decidable (a = b))
Decidability of Membership in Singleton Sets
Informal description
For any type $\alpha$ and elements $a, b \in \alpha$, if equality between $a$ and $b$ is decidable, then membership of $a$ in the singleton set $\{b\}$ is also decidable.
Prop.compl_singleton theorem
(p : Prop) : ({ p }ᶜ : Set Prop) = {¬p}
Full source 
@[simp] theorem Prop.compl_singleton (p : Prop) : ({p}{p}ᶜ : Set Prop) = {¬p} :=
  ext fun q ↦ by simpa [@Iff.comm q] using not_iff
Complement of Singleton Proposition Set Equals Singleton of Negation
Informal description
For any proposition $p$, the complement of the singleton set $\{p\}$ in the type of propositions is equal to the singleton set $\{\neg p\}$, i.e., $\{p\}^c = \{\neg p\}$.