mathlib3 documentation

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

P x

theorem set.bex_insert_iff {α : Type u} {P : α → Prop} {a : α} {s : set α} :

(∃ (x : α) (H : x ∈ has_insert.insert a s), P x) ↔ P a ∨ ∃ (x : α) (H : x ∈ s), P x

theorem set.ball_insert_iff {α : Type u} {P : α → Prop} {a : α} {s : set α} :

(∀ (x : α), x ∈ has_insert.insert a s → P x) ↔ P a ∧ ∀ (x : α), x ∈ s → P x

theorem set.singleton_def {α : Type u} (a : α) :

{a} = {a}

@[simp]

theorem set.mem_singleton_iff {α : Type u} {a b : α} :

a ∈ {b} ↔ a = b

@[simp]

theorem set.set_of_eq_eq_singleton {α : Type u} {a : α} :

{n : α | n = a} = {a}

@[simp]

theorem set.set_of_eq_eq_singleton' {α : Type u} {a : α} :

{x : α | a = x} = {a}

@[simp]

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

function.injective has_singleton.singleton

theorem set.singleton_injective {α : Type u} :

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

x ∈ {y}

theorem set.insert_eq {α : Type u} (x : α) (s : set α) :

has_insert.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} ≠ ∅

@[simp]

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.set_compr_eq_eq_singleton {α : Type u} {a : α} :

{b : α | b = a} = {a}

@[simp]

theorem set.singleton_union {α : Type u} {a : α} {s : set α} :

{a} ∪ s = has_insert.insert a s

@[simp]

theorem set.union_singleton {α : Type u} {a : α} {s : set α} :

s ∪ {a} = has_insert.insert a s

@[simp]

theorem set.singleton_inter_nonempty {α : Type u} {a : α} {s : set α} :

({a} ∩ s).nonempty ↔ a ∈ s

@[simp]

theorem set.inter_singleton_nonempty {α : Type u} {a : α} {s : set α} :

(s ∩ {a}).nonempty ↔ a ∈ s

@[simp]

theorem set.singleton_inter_eq_empty {α : Type u} {a : α} {s : set α} :

{a} ∩ s = ∅ ↔ a ∉ s

@[simp]

theorem set.inter_singleton_eq_empty {α : Type u} {a : α} {s : set α} :

s ∩ {a} = ∅ ↔ a ∉ s

theorem set.nmem_singleton_empty {α : Type u} {s : set α} :

s ∉ {∅} ↔ s.nonempty

@[protected, instance]

def set.unique_singleton {α : Type u} (a : α) :

unique ↥{a}

Equations

set.unique_singleton a = {to_inhabited := {default := ⟨a, _⟩}, uniq := _}

theorem set.eq_singleton_iff_unique_mem {α : Type u} {a : α} {s : set α} :

s = {a} ↔ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a

theorem set.eq_singleton_iff_nonempty_unique_mem {α : Type u} {a : α} {s : set α} :

s = {a} ↔ s.nonempty ∧ ∀ (x : α), x ∈ s → x = a

@[simp]

theorem set.default_coe_singleton {α : Type u} (x : α) :

inhabited.default = ⟨x, _⟩

@[simp]

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.mem_sep {α : Type u} {s : set α} {p : α → Prop} {x : α} (xs : x ∈ s) (px : p x) :

x ∈ {x ∈ s | p x}

@[simp]

theorem set.sep_mem_eq {α : Type u} {s t : set α} :

{x ∈ s | x ∈ t} = s ∩ t

@[simp]

theorem set.mem_sep_iff {α : Type u} {s : set α} {p : α → Prop} {x : α} :

x ∈ {x ∈ s | p x} ↔ x ∈ s ∧ p x

theorem set.sep_ext_iff {α : Type u} {s : set α} {p q : α → Prop} :

{x ∈ s | p x} = {x ∈ s | q x} ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)

theorem set.sep_eq_of_subset {α : Type u} {s t : set α} (h : s ⊆ t) :

{x ∈ t | x ∈ s} = s

@[simp]

theorem set.sep_subset {α : Type u} (s : set α) (p : α → Prop) :

{x ∈ s | p x} ⊆ s

@[simp]

theorem set.sep_eq_self_iff_mem_true {α : Type u} {s : set α} {p : α → Prop} :

{x ∈ s | p x} = s ↔ ∀ (x : α), x ∈ s → p x

@[simp]

theorem set.sep_eq_empty_iff_mem_false {α : Type u} {s : set α} {p : α → Prop} :

{x ∈ s | p x} = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x

@[simp]

theorem set.sep_true {α : Type u} {s : set α} :

{x ∈ s | true} = s

@[simp]

theorem set.sep_false {α : Type u} {s : set α} :

{x ∈ s | false} = ∅

@[simp]

theorem set.sep_empty {α : Type u} (p : α → Prop) :

{x ∈ ∅ | p x} = ∅

@[simp]

theorem set.sep_univ {α : Type u} {p : α → Prop} :

{x ∈ set.univ | p x} = {x : α | p x}

@[simp]

theorem set.sep_union {α : Type u} {s t : set α} {p : α → Prop} :

{x ∈ s ∪ t | p x} = {x ∈ s | p x} ∪ {x ∈ t | p x}

@[simp]

theorem set.sep_inter {α : Type u} {s t : set α} {p : α → Prop} :

{x ∈ s ∩ t | p x} = {x ∈ s | p x} ∩ {x ∈ t | p x}

@[simp]

theorem set.sep_and {α : Type u} {s : set α} {p q : α → Prop} :

{x ∈ s | p x ∧ q x} = {x ∈ s | p x} ∩ {x ∈ s | q x}

@[simp]

theorem set.sep_or {α : Type u} {s : set α} {p q : α → Prop} :

{x ∈ s | p x ∨ q x} = {x ∈ s | p x} ∪ {x ∈ s | q x}

@[simp]

theorem set.sep_set_of {α : Type u} {p q : α → Prop} :

{x ∈ {y : α | p y} | q x} = {x : α | p x ∧ q x}

@[simp]

theorem set.subset_singleton_iff {α : Type u_1} {s : set α} {x : α} :

s ⊆ {x} ↔ ∀ (y : α), 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} {a : α} {s : set α} (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 = ∅

@[protected]

theorem set.disjoint_iff {α : Type u} {s t : set α} :

disjoint s t ↔ s ∩ t ⊆ ∅

theorem set.disjoint_iff_inter_eq_empty {α : Type u} {s t : set α} :

disjoint s t ↔ s ∩ t = ∅

theorem disjoint.inter_eq {α : Type u} {s t : set α} :

disjoint s t → s ∩ t = ∅

theorem set.disjoint_left {α : Type u} {s t : set α} :

disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t

theorem set.disjoint_right {α : Type u} {s t : set α} :

disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s

theorem set.not_disjoint_iff {α : Type u} {s t : set α} :

¬disjoint s t ↔ ∃ (x : α), x ∈ s ∧ x ∈ t

theorem set.not_disjoint_iff_nonempty_inter {α : Type u} {s t : set α} :

¬disjoint s t ↔ (s ∩ t).nonempty

theorem set.nonempty.not_disjoint {α : Type u} {s t : set α} :

(s ∩ t).nonempty → ¬disjoint s t

Alias of the reverse direction of set.not_disjoint_iff_nonempty_inter.

theorem set.disjoint_or_nonempty_inter {α : Type u} (s t : set α) :

disjoint s t ∨ (s ∩ t).nonempty

theorem set.disjoint_iff_forall_ne {α : Type u} {s t : set α} :

disjoint s t ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x ≠ y

theorem disjoint.ne_of_mem {α : Type u} {s t : set α} (h : disjoint s t) {x y : α} (hx : x ∈ s) (hy : y ∈ t) :

x ≠ y

theorem set.disjoint_of_subset_left {α : Type u} {s₁ s₂ t : set α} (hs : s₁ ⊆ s₂) (h : disjoint s₂ t) :

disjoint s₁ t

theorem set.disjoint_of_subset_right {α : Type u} {s t₁ t₂ : set α} (ht : t₁ ⊆ t₂) (h : disjoint s t₂) :

disjoint s t₁

theorem set.disjoint_of_subset {α : Type u} {s₁ s₂ t₁ t₂ : set α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (h : disjoint s₂ t₂) :

disjoint s₁ t₁

@[simp]

theorem set.disjoint_union_left {α : Type u} {s t u : set α} :

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

@[simp]

theorem set.disjoint_union_right {α : Type u} {s t u : set α} :

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

@[simp]

theorem set.disjoint_empty {α : Type u} (s : set α) :

disjoint s ∅

@[simp]

theorem set.empty_disjoint {α : Type u} (s : set α) :

disjoint ∅ s

@[simp]

theorem set.univ_disjoint {α : Type u} {s : set α} :

disjoint set.univ s ↔ s = ∅

@[simp]

theorem set.disjoint_univ {α : Type u} {s : set α} :

disjoint s set.univ ↔ s = ∅

theorem set.disjoint_sdiff_left {α : Type u} {s t : set α} :

disjoint (t \ s) s

theorem set.disjoint_sdiff_right {α : Type u} {s t : set α} :

disjoint s (t \ s)

theorem set.diff_union_diff_cancel {α : Type u} {s t u : set α} (hts : t ⊆ s) (hut : u ⊆ t) :

s \ t ∪ t \ u = s \ u

theorem set.diff_diff_eq_sdiff_union {α : Type u} {s t u : set α} (h : u ⊆ s) :

s \ (t \ u) = s \ t ∪ u

@[simp]

theorem set.disjoint_singleton_left {α : Type u} {a : α} {s : set α} :

disjoint {a} s ↔ a ∉ s

@[simp]

theorem set.disjoint_singleton_right {α : Type u} {a : α} {s : set α} :

disjoint s {a} ↔ a ∉ s

@[simp]

theorem set.disjoint_singleton {α : Type u} {a b : α} :

disjoint {a} {b} ↔ a ≠ b

theorem set.subset_diff {α : Type u} {s t u : set α} :

s ⊆ t \ u ↔ s ⊆ t ∧ disjoint s u

theorem set.inter_diff_distrib_left {α : Type u} (s t u : set α) :

s ∩ (t \ u) = s ∩ t \ (s ∩ u)

theorem set.inter_diff_distrib_right {α : Type u} (s t u : set α) :

s \ t ∩ u = s ∩ u \ (t ∩ u)

theorem set.compl_def {α : Type u} (s : set α) :

sᶜ = {x : α | x ∉ s}

theorem set.mem_compl {α : Type u} {s : set α} {x : α} (h : x ∉ s) :

x ∈ sᶜ

theorem set.compl_set_of {α : Type u_1} (p : α → Prop) :

{a : α | p a}ᶜ = {a : α | ¬p a}

theorem set.not_mem_of_mem_compl {α : Type u} {s : set α} {x : α} (h : x ∈ sᶜ) :

x ∉ s

@[simp]

theorem set.mem_compl_iff {α : Type u} (s : set α) (x : α) :

x ∈ sᶜ ↔ x ∉ s

theorem set.not_mem_compl_iff {α : Type u} {s : set α} {x : α} :

x ∉ sᶜ ↔ x ∈ s

@[simp]

theorem set.inter_compl_self {α : Type u} (s : set α) :

s ∩ sᶜ = ∅

@[simp]

theorem set.compl_inter_self {α : Type u} (s : set α) :

sᶜ ∩ s = ∅

@[simp]

theorem set.compl_empty {α : Type u} :

∅ᶜ = set.univ

@[simp]

theorem set.compl_union {α : Type u} (s t : set α) :

(s ∪ t)ᶜ = sᶜ ∩ tᶜ

theorem set.compl_inter {α : Type u} (s t : set α) :

(s ∩ t)ᶜ = sᶜ ∪ tᶜ

@[simp]

theorem set.compl_univ {α : Type u} :

set.univ ᶜ = ∅

@[simp]

theorem set.compl_empty_iff {α : Type u} {s : set α} :

sᶜ = ∅ ↔ s = set.univ

@[simp]

theorem set.compl_univ_iff {α : Type u} {s : set α} :

sᶜ = set.univ ↔ s = ∅

theorem set.compl_ne_univ {α : Type u} {s : set α} :

sᶜ ≠ set.univ ↔ s.nonempty

theorem set.nonempty_compl {α : Type u} {s : set α} :

sᶜ.nonempty ↔ s ≠ set.univ

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}

theorem set.union_eq_compl_compl_inter_compl {α : Type u} (s t : set α) :

s ∪ t = (sᶜ ∩ tᶜ)ᶜ

theorem set.inter_eq_compl_compl_union_compl {α : Type u} (s t : set α) :

s ∩ t = (sᶜ ∪ tᶜ)ᶜ

@[simp]

theorem set.union_compl_self {α : Type u} (s : set α) :

s ∪ sᶜ = set.univ

@[simp]

theorem set.compl_union_self {α : Type u} (s : set α) :

sᶜ ∪ s = set.univ

theorem set.compl_subset_comm {α : Type u} {s t : set α} :

sᶜ ⊆ t ↔ tᶜ ⊆ s

theorem set.subset_compl_comm {α : Type u} {s t : set α} :

s ⊆ tᶜ ↔ t ⊆ sᶜ

@[simp]

theorem set.compl_subset_compl {α : Type u} {s t : set α} :

sᶜ ⊆ tᶜ ↔ t ⊆ s

theorem set.subset_compl_iff_disjoint_left {α : Type u} {s t : set α} :

s ⊆ tᶜ ↔ disjoint t s

theorem set.subset_compl_iff_disjoint_right {α : Type u} {s t : set α} :

s ⊆ tᶜ ↔ disjoint s t

theorem set.disjoint_compl_left_iff_subset {α : Type u} {s t : set α} :

disjoint sᶜ t ↔ t ⊆ s

theorem set.disjoint_compl_right_iff_subset {α : Type u} {s t : set α} :

disjoint s tᶜ ↔ s ⊆ t

theorem disjoint.subset_compl_right {α : Type u} {s t : set α} :

disjoint s t → s ⊆ tᶜ

Alias of the reverse direction of set.subset_compl_iff_disjoint_right.

theorem disjoint.subset_compl_left {α : Type u} {s t : set α} :

disjoint t s → s ⊆ tᶜ

Alias of the reverse direction of set.subset_compl_iff_disjoint_left.

theorem has_subset.subset.disjoint_compl_left {α : Type u} {s t : set α} :

t ⊆ s → disjoint sᶜ t

Alias of the reverse direction of set.disjoint_compl_left_iff_subset.

theorem has_subset.subset.disjoint_compl_right {α : Type u} {s t : set α} :

s ⊆ t → disjoint s tᶜ

Alias of the reverse direction of set.disjoint_compl_right_iff_subset.

theorem set.subset_union_compl_iff_inter_subset {α : Type u} {s t u : set α} :

s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t

theorem set.compl_subset_iff_union {α : Type u} {s t : set α} :

sᶜ ⊆ t ↔ s ∪ t = set.univ

@[simp]

theorem set.subset_compl_singleton_iff {α : Type u} {a : α} {s : set α} :

s ⊆ {a}ᶜ ↔ a ∉ s

theorem set.inter_subset {α : Type u} (a b c : set α) :

a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c

theorem set.inter_compl_nonempty_iff {α : Type u} {s t : set α} :

(s ∩ tᶜ).nonempty ↔ ¬s ⊆ t

theorem set.diff_eq {α : Type u} (s t : set α) :

s \ t = s ∩ tᶜ

@[simp]

theorem set.mem_diff {α : Type u} {s t : set α} (x : α) :

x ∈ s \ t ↔ x ∈ s ∧ x ∉ t

theorem set.mem_diff_of_mem {α : Type u} {s t : set α} {x : α} (h1 : x ∈ s) (h2 : x ∉ t) :

x ∈ s \ t

theorem set.not_mem_diff_of_mem {α : Type u} {s t : set α} {x : α} (hx : x ∈ t) :

x ∉ s \ t

theorem set.mem_of_mem_diff {α : Type u} {s t : set α} {x : α} (h : x ∈ s \ t) :

x ∈ s

theorem set.not_mem_of_mem_diff {α : Type u} {s t : set α} {x : α} (h : x ∈ s \ t) :

x ∉ t

theorem set.diff_eq_compl_inter {α : Type u} {s t : set α} :

s \ t = tᶜ ∩ s

theorem set.nonempty_diff {α : Type u} {s t : set α} :

(s \ t).nonempty ↔ ¬s ⊆ t

theorem set.diff_subset {α : Type u} (s t : set α) :

s \ t ⊆ s

theorem set.union_diff_cancel' {α : Type u} {s t u : set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) :

t ∪ u \ s = u

theorem set.union_diff_cancel {α : Type u} {s t : set α} (h : s ⊆ t) :

s ∪ t \ s = t

theorem set.union_diff_cancel_left {α : Type u} {s t : set α} (h : s ∩ t ⊆ ∅) :

(s ∪ t) \ s = t

theorem set.union_diff_cancel_right {α : Type u} {s t : set α} (h : s ∩ t ⊆ ∅) :

(s ∪ t) \ t = s

@[simp]

theorem set.union_diff_left {α : Type u} {s t : set α} :

(s ∪ t) \ s = t \ s

@[simp]

theorem set.union_diff_right {α : Type u} {s t : set α} :

(s ∪ t) \ t = s \ t

theorem set.union_diff_distrib {α : Type u} {s t u : set α} :

(s ∪ t) \ u = s \ u ∪ t \ u

theorem set.inter_diff_assoc {α : Type u} (a b c : set α) :

a ∩ b \ c = a ∩ (b \ c)

@[simp]

theorem set.inter_diff_self {α : Type u} (a b : set α) :

a ∩ (b \ a) = ∅

@[simp]

theorem set.inter_union_diff {α : Type u} (s t : set α) :

s ∩ t ∪ s \ t = s

@[simp]

theorem set.diff_union_inter {α : Type u} (s t : set α) :

s \ t ∪ s ∩ t = s

@[simp]

theorem set.inter_union_compl {α : Type u} (s t : set α) :

s ∩ t ∪ s ∩ tᶜ = s

theorem set.diff_subset_diff {α : Type u} {s₁ s₂ t₁ t₂ : set α} :

s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂

theorem set.diff_subset_diff_left {α : Type u} {s₁ s₂ t : set α} (h : s₁ ⊆ s₂) :

s₁ \ t ⊆ s₂ \ t

theorem set.diff_subset_diff_right {α : Type u} {s t u : set α} (h : t ⊆ u) :

s \ u ⊆ s \ t

theorem set.compl_eq_univ_diff {α : Type u} (s : set α) :

sᶜ = set.univ \ s

@[simp]

theorem set.empty_diff {α : Type u} (s : set α) :

∅ \ s = ∅

theorem set.diff_eq_empty {α : Type u} {s t : set α} :

s \ t = ∅ ↔ s ⊆ t

@[simp]

theorem set.diff_empty {α : Type u} {s : set α} :

s \ ∅ = s

@[simp]

theorem set.diff_univ {α : Type u} (s : set α) :

s \ set.univ = ∅

theorem set.diff_diff {α : Type u} {s t u : set α} :

s \ t \ u = s \ (t ∪ u)

theorem set.diff_diff_comm {α : Type u} {s t u : set α} :

s \ t \ u = s \ u \ t

theorem set.diff_subset_iff {α : Type u} {s t u : set α} :

s \ t ⊆ u ↔ s ⊆ t ∪ u

theorem set.subset_diff_union {α : Type u} (s t : set α) :

s ⊆ s \ t ∪ t

theorem set.diff_union_of_subset {α : Type u} {s t : set α} (h : t ⊆ s) :

s \ t ∪ t = s

@[simp]

theorem set.diff_singleton_subset_iff {α : Type u} {x : α} {s t : set α} :

s \ {x} ⊆ t ↔ s ⊆ has_insert.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 ⊆ has_insert.insert x (s \ {x})

theorem set.diff_subset_comm {α : Type u} {s t u : set α} :

s \ t ⊆ u ↔ s \ u ⊆ t

theorem set.diff_inter {α : Type u} {s t u : set α} :

s \ (t ∩ u) = s \ t ∪ s \ u

theorem set.diff_inter_diff {α : Type u} {s t u : set α} :

s \ t ∩ (s \ u) = s \ (t ∪ u)

theorem set.diff_compl {α : Type u} {s t : set α} :

s \ tᶜ = s ∩ t

theorem set.diff_diff_right {α : Type u} {s t u : set α} :

s \ (t \ u) = s \ t ∪ s ∩ u

@[simp]

theorem set.insert_diff_of_mem {α : Type u} {a : α} {t : set α} (s : set α) (h : a ∈ t) :

has_insert.insert a s \ t = s \ t

theorem set.insert_diff_of_not_mem {α : Type u} {a : α} {t : set α} (s : set α) (h : a ∉ t) :

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

theorem set.insert_diff_self_of_not_mem {α : Type u} {a : α} {s : set α} (h : a ∉ s) :

has_insert.insert a s \ {a} = s

@[simp]

theorem set.insert_diff_eq_singleton {α : Type u} {a : α} {s : set α} (h : a ∉ s) :

has_insert.insert a s \ s = {a}

theorem set.inter_insert_of_mem {α : Type u} {a : α} {s t : set α} (h : a ∈ s) :

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

theorem set.insert_inter_of_mem {α : Type u} {a : α} {s t : set α} (h : a ∈ t) :

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

theorem set.inter_insert_of_not_mem {α : Type u} {a : α} {s t : set α} (h : a ∉ s) :

s ∩ has_insert.insert a t = s ∩ t

theorem set.insert_inter_of_not_mem {α : Type u} {a : α} {s t : set α} (h : a ∉ t) :

has_insert.insert a s ∩ t = s ∩ t

@[simp]

theorem set.union_diff_self {α : Type u} {s t : set α} :

s ∪ t \ s = s ∪ t

@[simp]

theorem set.diff_union_self {α : Type u} {s t : set α} :

s \ t ∪ t = s ∪ t

@[simp]

theorem set.diff_inter_self {α : Type u} {a b : set α} :

b \ a ∩ a = ∅

@[simp]

theorem set.diff_inter_self_eq_diff {α : Type u} {s t : set α} :

s \ (t ∩ s) = s \ t

@[simp]

theorem set.diff_self_inter {α : Type u} {s t : set α} :

s \ (s ∩ t) = s \ t

@[simp]

theorem set.diff_singleton_eq_self {α : Type u} {a : α} {s : set α} (h : a ∉ s) :

s \ {a} = s

@[simp]

theorem set.diff_singleton_ssubset {α : Type u} {s : set α} {a : α} :

s \ {a} ⊂ s ↔ a ∈ s

@[simp]

theorem set.insert_diff_singleton {α : Type u} {a : α} {s : set α} :

has_insert.insert a (s \ {a}) = has_insert.insert a s

theorem set.insert_diff_singleton_comm {α : Type u} {a b : α} (hab : a ≠ b) (s : set α) :

has_insert.insert a (s \ {b}) = has_insert.insert a s \ {b}

@[simp]

theorem set.diff_self {α : Type u} {s : set α} :

s \ s = ∅

theorem set.diff_diff_right_self {α : Type u} (s t : set α) :

s \ (s \ t) = s ∩ t

theorem set.diff_diff_cancel_left {α : Type u} {s t : set α} (h : s ⊆ t) :

t \ (t \ s) = s

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.union_eq_diff_union_diff_union_inter {α : Type u} (s t : set α) :

s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

theorem set.mem_symm_diff {α : Type u} {a : α} {s t : set α} :

a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

@[protected]

theorem set.symm_diff_def {α : Type u} (s t : set α) :

s ∆ t = s \ t ∪ t \ s

theorem set.symm_diff_subset_union {α : Type u} {s t : set α} :

s ∆ t ⊆ s ∪ t

@[simp]

theorem set.symm_diff_eq_empty {α : Type u} {s t : set α} :

s ∆ t = ∅ ↔ s = t

@[simp]

theorem set.symm_diff_nonempty {α : Type u} {s t : set α} :

(s ∆ t).nonempty ↔ s ≠ t

theorem set.inter_symm_diff_distrib_left {α : Type u} (s t u : set α) :

s ∩ t ∆ u = (s ∩ t) ∆ (s ∩ u)

theorem set.inter_symm_diff_distrib_right {α : Type u} (s t u : set α) :

s ∆ t ∩ u = (s ∩ u) ∆ (t ∩ u)

theorem set.subset_symm_diff_union_symm_diff_left {α : Type u} {s t u : set α} (h : disjoint s t) :

u ⊆ s ∆ u ∪ t ∆ u

theorem set.subset_symm_diff_union_symm_diff_right {α : Type u} {s t u : set α} (h : disjoint t u) :

s ⊆ s ∆ t ∪ s ∆ u

def set.powerset {α : Type u} (s : set α) :

set (set α)

𝒫 s = set.powerset s is the set of all subsets of s.

Equations

𝒫s = {t : set α | t ⊆ s}

theorem set.mem_powerset {α : Type u} {x s : set α} (h : x ⊆ s) :

x ∈ 𝒫s

theorem set.subset_of_mem_powerset {α : Type u} {x s : set α} (h : x ∈ 𝒫s) :

x ⊆ s

@[simp]

theorem set.mem_powerset_iff {α : Type u} (x s : set α) :

x ∈ 𝒫s ↔ x ⊆ s

theorem set.powerset_inter {α : Type u} (s t : set α) :

𝒫(s ∩ t) = 𝒫s ∩ 𝒫t

@[simp]

theorem set.powerset_mono {α : Type u} {s t : set α} :

𝒫s ⊆ 𝒫t ↔ s ⊆ t

theorem set.monotone_powerset {α : Type u} :

monotone set.powerset

@[simp]

theorem set.powerset_nonempty {α : Type u} {s : set α} :

(𝒫s).nonempty

@[simp]

theorem set.powerset_empty {α : Type u} :

𝒫 ∅ = {∅}

@[simp]

theorem set.powerset_univ {α : Type u} :

𝒫 set.univ = set.univ

theorem set.powerset_singleton {α : Type u} (x : α) :

𝒫{x} = {∅, {x}}

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

theorem set.mem_dite_univ_right {α : Type u} (p : Prop) [decidable p] (t : p → set α) (x : α) :

x ∈ dite p (λ (h : p), t h) (λ (h : ¬p), set.univ) ↔ ∀ (h : p), x ∈ t h

@[simp]

theorem set.mem_ite_univ_right {α : Type u} (p : Prop) [decidable p] (t : set α) (x : α) :

x ∈ ite p t set.univ ↔ p → x ∈ t

theorem set.mem_dite_univ_left {α : Type u} (p : Prop) [decidable p] (t : ¬p → set α) (x : α) :

x ∈ dite p (λ (h : p), set.univ) (λ (h : ¬p), t h) ↔ ∀ (h : ¬p), x ∈ t h

@[simp]

theorem set.mem_ite_univ_left {α : Type u} (p : Prop) [decidable p] (t : set α) (x : α) :

x ∈ ite p set.univ t ↔ ¬p → x ∈ t

theorem set.mem_dite_empty_right {α : Type u} (p : Prop) [decidable p] (t : p → set α) (x : α) :

x ∈ dite p (λ (h : p), t h) (λ (h : ¬p), ∅) ↔ ∃ (h : p), x ∈ t h

@[simp]

theorem set.mem_ite_empty_right {α : Type u} (p : Prop) [decidable p] (t : set α) (x : α) :

x ∈ ite p t ∅ ↔ p ∧ x ∈ t

theorem set.mem_dite_empty_left {α : Type u} (p : Prop) [decidable p] (t : ¬p → set α) (x : α) :

x ∈ dite p (λ (h : p), ∅) (λ (h : ¬p), t h) ↔ ∃ (h : ¬p), x ∈ t h

@[simp]

theorem set.mem_ite_empty_left {α : Type u} (p : Prop) [decidable p] (t : set α) (x : α) :

x ∈ ite p ∅ t ↔ ¬p ∧ x ∈ t

@[protected]

def set.ite {α : Type u} (t s s' : set α) :

set α

ite for sets: set.ite t s s' ∩ t = s ∩ t, set.ite t s s' ∩ tᶜ = s' ∩ tᶜ. Defined as s ∩ t ∪ s' \ t.

Equations

t.ite s s' = s ∩ t ∪ s' \ t

@[simp]

theorem set.ite_inter_self {α : Type u} (t s s' : set α) :

t.ite s s' ∩ t = s ∩ t

@[simp]

theorem set.ite_compl {α : Type u} (t s s' : set α) :

tᶜ.ite s s' = t.ite s' s

@[simp]

theorem set.ite_inter_compl_self {α : Type u} (t s s' : set α) :

t.ite s s' ∩ tᶜ = s' ∩ tᶜ

@[simp]

theorem set.ite_diff_self {α : Type u} (t s s' : set α) :

t.ite s s' \ t = s' \ t

@[simp]

theorem set.ite_same {α : Type u} (t s : set α) :

t.ite s s = s

@[simp]

theorem set.ite_left {α : Type u} (s t : set α) :

s.ite s t = s ∪ t

@[simp]

theorem set.ite_right {α : Type u} (s t : set α) :

s.ite t s = t ∩ s

@[simp]

theorem set.ite_empty {α : Type u} (s s' : set α) :

∅.ite s s' = s'

@[simp]

theorem set.ite_univ {α : Type u} (s s' : set α) :

set.univ.ite s s' = s

@[simp]

theorem set.ite_empty_left {α : Type u} (t s : set α) :

t.ite ∅ s = s \ t

@[simp]

theorem set.ite_empty_right {α : Type u} (t s : set α) :

t.ite s ∅ = s ∩ t

theorem set.ite_mono {α : Type u} (t : set α) {s₁ s₁' s₂ s₂' : set α} (h : s₁ ⊆ s₂) (h' : s₁' ⊆ s₂') :

t.ite s₁ s₁' ⊆ t.ite s₂ s₂'

theorem set.ite_subset_union {α : Type u} (t s s' : set α) :

t.ite s s' ⊆ s ∪ s'

theorem set.inter_subset_ite {α : Type u} (t s s' : set α) :

s ∩ s' ⊆ t.ite s s'

theorem set.ite_inter_inter {α : Type u} (t s₁ s₂ s₁' s₂' : set α) :

t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'

theorem set.ite_inter {α : Type u} (t s₁ s₂ s : set α) :

t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s

theorem set.ite_inter_of_inter_eq {α : Type u} (t : set α) {s₁ s₂ s : set α} (h : s₁ ∩ s = s₂ ∩ s) :

t.ite s₁ s₂ ∩ s = s₁ ∩ s

theorem set.subset_ite {α : Type u} {t s s' u : set α} :

u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'

@[protected]

def set.subsingleton {α : Type u} (s : set α) :

Prop

A set s is a subsingleton if it has at most one element.

Equations

s.subsingleton = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

theorem set.subsingleton.anti {α : Type u} {s t : set α} (ht : t.subsingleton) (hst : s ⊆ t) :

theorem set.subsingleton.eq_singleton_of_mem {α : Type u} {s : set α} (hs : s.subsingleton) {x : α} (hx : x ∈ s) :

s = {x}

@[simp]

theorem set.subsingleton_empty {α : Type u} :

∅.subsingleton

@[simp]

theorem set.subsingleton_singleton {α : Type u} {a : α} :

{a}.subsingleton

theorem set.subsingleton_of_subset_singleton {α : Type u} {a : α} {s : set α} (h : s ⊆ {a}) :

theorem set.subsingleton_of_forall_eq {α : Type u} {s : set α} (a : α) (h : ∀ (b : α), b ∈ s → b = a) :

theorem set.subsingleton_iff_singleton {α : Type u} {s : set α} {x : α} (hx : x ∈ s) :

s.subsingleton ↔ s = {x}

theorem set.subsingleton.eq_empty_or_singleton {α : Type u} {s : set α} (hs : s.subsingleton) :

s = ∅ ∨ ∃ (x : α), s = {x}

theorem set.subsingleton.induction_on {α : Type u} {s : set α} {p : set α → Prop} (hs : s.subsingleton) (he : p ∅) (h₁ : ∀ (x : α), p {x}) :

p s

theorem set.subsingleton_univ {α : Type u} [subsingleton α] :

set.univ.subsingleton

theorem set.subsingleton_of_univ_subsingleton {α : Type u} (h : set.univ.subsingleton) :

subsingleton α

@[simp]

theorem set.subsingleton_univ_iff {α : Type u} :

set.univ.subsingleton ↔ subsingleton α

theorem set.subsingleton_of_subsingleton {α : Type u} [subsingleton α] {s : set α} :

theorem set.subsingleton_is_top (α : Type u_1) [partial_order α] :

{x : α | is_top x}.subsingleton

theorem set.subsingleton_is_bot (α : Type u_1) [partial_order α] :

{x : α | is_bot x}.subsingleton

theorem set.exists_eq_singleton_iff_nonempty_subsingleton {α : Type u} {s : set α} :

(∃ (a : α), s = {a}) ↔ s.nonempty ∧ s.subsingleton

@[simp, norm_cast]

theorem set.subsingleton_coe {α : Type u} (s : set α) :

subsingleton ↥s ↔ s.subsingleton

s, coerced to a type, is a subsingleton type if and only if s is a subsingleton set.

theorem set.subsingleton.coe_sort {α : Type u} {s : set α} :

s.subsingleton → subsingleton ↥s

@[protected, instance]

def set.subsingleton_coe_of_subsingleton {α : Type u} [subsingleton α] {s : set α} :

subsingleton ↥s

The coe_sort of a set s in a subsingleton type is a subsingleton. For the corresponding result for subtype, see subtype.subsingleton.

@[protected]

def set.nontrivial {α : Type u} (s : set α) :

Prop

A set s is nontrivial if it has at least two distinct elements.

Equations

s.nontrivial = ∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x ≠ y

theorem set.nontrivial_of_mem_mem_ne {α : Type u} {s : set α} {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) :

@[protected]

noncomputable def set.nontrivial.some {α : Type u} {s : set α} (hs : s.nontrivial) :

α × α

Extract witnesses from s.nontrivial. This function might be used instead of case analysis on the argument. Note that it makes a proof depend on the classical.choice axiom.

Equations

hs.some = (Exists.some hs, Exists.some _)

@[protected]

theorem set.nontrivial.some_fst_mem {α : Type u} {s : set α} (hs : s.nontrivial) :

hs.some.fst ∈ s

@[protected]

theorem set.nontrivial.some_snd_mem {α : Type u} {s : set α} (hs : s.nontrivial) :

hs.some.snd ∈ s

@[protected]

theorem set.nontrivial.some_fst_ne_some_snd {α : Type u} {s : set α} (hs : s.nontrivial) :

hs.some.fst ≠ hs.some.snd

theorem set.nontrivial.mono {α : Type u} {s t : set α} (hs : s.nontrivial) (hst : s ⊆ t) :

t.nontrivial

theorem set.nontrivial_pair {α : Type u} {x y : α} (hxy : x ≠ y) :

{x, y}.nontrivial

theorem set.nontrivial_of_pair_subset {α : Type u} {s : set α} {x y : α} (hxy : x ≠ y) (h : {x, y} ⊆ s) :

theorem set.nontrivial.pair_subset {α : Type u} {s : set α} (hs : s.nontrivial) :

∃ (x y : α) (hab : x ≠ y), {x, y} ⊆ s

theorem set.nontrivial_iff_pair_subset {α : Type u} {s : set α} :

s.nontrivial ↔ ∃ (x y : α) (hxy : x ≠ y), {x, y} ⊆ s

theorem set.nontrivial_of_exists_ne {α : Type u} {s : set α} {x : α} (hx : x ∈ s) (h : ∃ (y : α) (H : y ∈ s), y ≠ x) :

theorem set.nontrivial.exists_ne {α : Type u} {s : set α} (hs : s.nontrivial) (z : α) :

∃ (x : α) (H : x ∈ s), x ≠ z

theorem set.nontrivial_iff_exists_ne {α : Type u} {s : set α} {x : α} (hx : x ∈ s) :

s.nontrivial ↔ ∃ (y : α) (H : y ∈ s), y ≠ x

theorem set.nontrivial_of_lt {α : Type u} {s : set α} [preorder α] {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : x < y) :

theorem set.nontrivial_of_exists_lt {α : Type u} {s : set α} [preorder α] (H : ∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x < y) :

theorem set.nontrivial.exists_lt {α : Type u} {s : set α} [linear_order α] (hs : s.nontrivial) :

∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x < y

theorem set.nontrivial_iff_exists_lt {α : Type u} {s : set α} [linear_order α] :

s.nontrivial ↔ ∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x < y

@[protected]

theorem set.nontrivial.nonempty {α : Type u} {s : set α} (hs : s.nontrivial) :

s.nonempty

@[protected]

theorem set.nontrivial.ne_empty {α : Type u} {s : set α} (hs : s.nontrivial) :

s ≠ ∅

theorem set.nontrivial.not_subset_empty {α : Type u} {s : set α} (hs : s.nontrivial) :

¬s ⊆ ∅

@[simp]

theorem set.not_nontrivial_empty {α : Type u} :

¬∅.nontrivial

@[simp]

theorem set.not_nontrivial_singleton {α : Type u} {x : α} :

¬{x}.nontrivial

theorem set.nontrivial.ne_singleton {α : Type u} {s : set α} {x : α} (hs : s.nontrivial) :

s ≠ {x}

theorem set.nontrivial.not_subset_singleton {α : Type u} {s : set α} {x : α} (hs : s.nontrivial) :

¬s ⊆ {x}

theorem set.nontrivial_univ {α : Type u} [nontrivial α] :

set.univ.nontrivial

theorem set.nontrivial_of_univ_nontrivial {α : Type u} (h : set.univ.nontrivial) :

nontrivial α

@[simp]

theorem set.nontrivial_univ_iff {α : Type u} :

set.univ.nontrivial ↔ nontrivial α

theorem set.nontrivial_of_nontrivial {α : Type u} {s : set α} (hs : s.nontrivial) :

nontrivial α

@[simp, norm_cast]

theorem set.nontrivial_coe_sort {α : Type u} {s : set α} :

nontrivial ↥s ↔ s.nontrivial

s, coerced to a type, is a nontrivial type if and only if s is a nontrivial set.

theorem set.nontrivial.coe_sort {α : Type u} {s : set α} :

s.nontrivial → nontrivial ↥s

Alias of the reverse direction of set.nontrivial_coe_sort.

theorem set.nontrivial_of_nontrivial_coe {α : Type u} {s : set α} (hs : nontrivial ↥s) :

nontrivial α

A type with a set s whose coe_sort is a nontrivial type is nontrivial. For the corresponding result for subtype, see subtype.nontrivial_iff_exists_ne.

theorem set.nontrivial_mono {α : Type u_1} {s t : set α} (hst : s ⊆ t) (hs : nontrivial ↥s) :

nontrivial ↥t

@[simp]

theorem set.not_subsingleton_iff {α : Type u} {s : set α} :

¬s.subsingleton ↔ s.nontrivial

@[simp]

theorem set.not_nontrivial_iff {α : Type u} {s : set α} :

¬s.nontrivial ↔ s.subsingleton

theorem set.subsingleton.not_nontrivial {α : Type u} {s : set α} :

s.subsingleton → ¬s.nontrivial

Alias of the reverse direction of set.not_nontrivial_iff.

theorem set.nontrivial.not_subsingleton {α : Type u} {s : set α} :

s.nontrivial → ¬s.subsingleton

Alias of the reverse direction of set.not_subsingleton_iff.

@[protected]

theorem set.subsingleton_or_nontrivial {α : Type u} (s : set α) :

s.subsingleton ∨ s.nontrivial

theorem set.eq_singleton_or_nontrivial {α : Type u} {a : α} {s : set α} (ha : a ∈ s) :

s = {a} ∨ s.nontrivial

theorem set.nontrivial_iff_ne_singleton {α : Type u} {a : α} {s : set α} (ha : a ∈ s) :

s.nontrivial ↔ s ≠ {a}

theorem set.nonempty.exists_eq_singleton_or_nontrivial {α : Type u} {s : set α} :

s.nonempty → (∃ (a : α), s = {a}) ∨ s.nontrivial

theorem set.univ_eq_true_false :

set.univ = {true, false}

theorem set.monotone_on_iff_monotone {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] {f : α → β} :

monotone_on f s ↔ monotone (λ (a : ↥s), f ↑a)

theorem set.antitone_on_iff_antitone {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] {f : α → β} :

antitone_on f s ↔ antitone (λ (a : ↥s), f ↑a)

theorem set.strict_mono_on_iff_strict_mono {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] {f : α → β} :

strict_mono_on f s ↔ strict_mono (λ (a : ↥s), f ↑a)

theorem set.strict_anti_on_iff_strict_anti {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] {f : α → β} :

strict_anti_on f s ↔ strict_anti (λ (a : ↥s), f ↑a)

@[protected]

theorem set.subsingleton.monotone_on {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] (f : α → β) (h : s.subsingleton) :

monotone_on f s

@[protected]

theorem set.subsingleton.antitone_on {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] (f : α → β) (h : s.subsingleton) :

antitone_on f s

@[protected]

theorem set.subsingleton.strict_mono_on {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] (f : α → β) (h : s.subsingleton) :

strict_mono_on f s

@[protected]

theorem set.subsingleton.strict_anti_on {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] (f : α → β) (h : s.subsingleton) :

strict_anti_on f s

@[simp]

theorem set.monotone_on_singleton {α : Type u} {β : Type v} {a : α} [preorder α] [preorder β] (f : α → β) :

monotone_on f {a}

@[simp]

theorem set.antitone_on_singleton {α : Type u} {β : Type v} {a : α} [preorder α] [preorder β] (f : α → β) :

antitone_on f {a}

@[simp]

theorem set.strict_mono_on_singleton {α : Type u} {β : Type v} {a : α} [preorder α] [preorder β] (f : α → β) :

strict_mono_on f {a}

@[simp]

theorem set.strict_anti_on_singleton {α : Type u} {β : Type v} {a : α} [preorder α] [preorder β] (f : α → β) :

strict_anti_on f {a}

theorem set.not_monotone_on_not_antitone_on_iff_exists_le_le {α : Type u} {β : Type v} {s : set α} [linear_order α] [linear_order β] {f : α → β} :

¬monotone_on f s ∧ ¬antitone_on f s ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ s) (c : α) (H : c ∈ s), a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.

theorem set.not_monotone_on_not_antitone_on_iff_exists_lt_lt {α : Type u} {β : Type v} {s : set α} [linear_order α] [linear_order β] {f : α → β} :

¬monotone_on f s ∧ ¬antitone_on f s ↔ ∃ (a : α) (H : a ∈ s) (b : α) (H : b ∈ s) (c : α) (H : c ∈ s), a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.