mathlib3 documentation

data.set.basic

Basic properties of sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Sets in Lean are homogeneous; all their elements have the same type. Sets whose elements have type X are thus defined as set X := X → Prop. Note that this function need not be decidable. The definition is in the core library.

This file provides some basic definitions related to sets and functions not present in the core library, as well as extra lemmas for functions in the core library (empty set, univ, union, intersection, insert, singleton, set-theoretic difference, complement, and powerset).

Note that a set is a term, not a type. There is a coercion from set α to Type* sending s to the corresponding subtype ↥s.

See also the file set_theory/zfc.lean, which contains an encoding of ZFC set theory in Lean.

Main definitions #

Notation used here:

Definitions in the file:

Notation #

Implementation notes #

Tags #

set, sets, subset, subsets, union, intersection, insert, singleton, complement, powerset

Set coercion to a type #

source
@[protected, instance]
def set.has_le {α : Type u_1} :
has_le (set α)
Equations
source
@[protected, instance]
def set.has_subset {α : Type u_1} :
has_subset (set α)
Equations
source
@[protected, instance]
def set.boolean_algebra {α : Type u_1} :
boolean_algebra (set α)
Equations
source
@[protected, instance]
def set.has_ssubset {α : Type u_1} :
has_ssubset (set α)
Equations
source
@[protected, instance]
def set.has_union {α : Type u_1} :
has_union (set α)
Equations
source
@[protected, instance]
def set.has_inter {α : Type u_1} :
has_inter (set α)
Equations
source
@[simp]
theorem set.top_eq_univ {α : Type u_1} :
⊤ = set.univ
source
@[simp]
theorem set.bot_eq_empty {α : Type u_1} :
⊥ = ∅
source
@[simp]
theorem set.sup_eq_union {α : Type u_1} :
has_sup.sup = has_union.union
source
@[simp]
theorem set.inf_eq_inter {α : Type u_1} :
has_inf.inf = has_inter.inter
source
@[simp]
theorem set.le_eq_subset {α : Type u_1} :
has_le.le = has_subset.subset
source
@[simp]
theorem set.lt_eq_ssubset {α : Type u_1} :
has_lt.lt = has_ssubset.ssubset
source
theorem set.le_iff_subset {α : Type u_1} {s t : set α} :
s ≤ t ↔ s ⊆ t
source
theorem set.lt_iff_ssubset {α : Type u_1} {s t : set α} :
s < t ↔ s ⊂ t
source
theorem has_le.le.subset {α : Type u_1} {s t : set α} :
s ≤ t → s ⊆ t

Alias of the forward direction of set.le_iff_subset.

source
theorem has_subset.subset.le {α : Type u_1} {s t : set α} :
s ⊆ t → s ≤ t

Alias of the reverse direction of set.le_iff_subset.

source
theorem has_ssubset.ssubset.lt {α : Type u_1} {s t : set α} :
s ⊂ t → s < t

Alias of the reverse direction of set.lt_iff_ssubset.

source
theorem has_lt.lt.ssubset {α : Type u_1} {s t : set α} :
s < t → s ⊂ t

Alias of the forward direction of set.lt_iff_ssubset.

source
@[protected, instance]
def set.has_coe_to_sort {α : Type u} :
has_coe_to_sort (set α) (Type u)

Coercion from a set to the corresponding subtype.

Equations
source
@[protected, instance]
def set.pi_set_coe.can_lift (ι : Type u) (α : ι → Type v) [ne : ∀ (i : ι), nonempty (α i)] (s : set ι) :
can_lift (Π (i : ↥s), α ↑i) (Π (i : ι), α i) (λ (f : Π (i : ι), α i) (i : ↥s), f ↑i) (λ (_x : Π (i : ↥s), α ↑i), true)
Equations
source
@[protected, instance]
def set.pi_set_coe.can_lift' (ι : Type u) (α : Type v) [ne : nonempty α] (s : set ι) :
can_lift (↥s → α) (ι → α) (λ (f : ι → α) (i : ↥s), f ↑i) (λ (_x : ↥s → α), true)
Equations
source
theorem set.coe_eq_subtype {α : Type u} (s : set α) :
↥s = {x // x ∈ s}
source
@[simp]
theorem set.coe_set_of {α : Type u} (p : α → Prop) :
↥{x : α | p x} = {x // p x}
source
@[simp]
theorem set_coe.forall {α : Type u} {s : set α} {p : ↥s → Prop} :
(∀ (x : ↥s), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩
source
@[simp]
theorem set_coe.exists {α : Type u} {s : set α} {p : ↥s → Prop} :
(∃ (x : ↥s), p x) ↔ ∃ (x : α) (h : x ∈ s), p ⟨x, h⟩
source
theorem set_coe.exists' {α : Type u} {s : set α} {p : Π (x : α), x ∈ s → Prop} :
(∃ (x : α) (h : x ∈ s), p x h) ↔ ∃ (x : ↥s), p ↑x _
source
theorem set_coe.forall' {α : Type u} {s : set α} {p : Π (x : α), x ∈ s → Prop} :
(∀ (x : α) (h : x ∈ s), p x h) ↔ ∀ (x : ↥s), p ↑x _
source
@[simp]
theorem set_coe_cast {α : Type u} {s t : set α} (H' : s = t) (H : ↥s = ↥t) (x : ↥s) :
cast H x = ⟨x.val, _⟩
source
theorem set_coe.ext {α : Type u} {s : set α} {a b : ↥s} :
↑a = ↑b → a = b
source
theorem set_coe.ext_iff {α : Type u} {s : set α} {a b : ↥s} :
↑a = ↑b ↔ a = b
source
theorem subtype.mem {α : Type u_1} {s : set α} (p : ↥s) :
↑p ∈ s

See also subtype.prop

source
theorem eq.subset {α : Type u_1} {s t : set α} :
s = t → s ⊆ t

Duplicate of eq.subset', which currently has elaboration problems.

source
@[protected, instance]
def set.inhabited {α : Type u} :
inhabited (set α)
Equations
source
@[ext]
theorem set.ext {α : Type u} {a b : set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) :
a = b
source
theorem set.ext_iff {α : Type u} {s t : set α} :
s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
source
@[trans]
theorem set.mem_of_mem_of_subset {α : Type u} {x : α} {s t : set α} (hx : x ∈ s) (h : s ⊆ t) :
x ∈ t
source
theorem set.forall_in_swap {α : Type u} {β : Type v} {s : set α} {p : α → β → Prop} :
(∀ (a : α), a ∈ s → ∀ (b : β), p a b) ↔ ∀ (b : β) (a : α), a ∈ s → p a b

Lemmas about mem and set_of #

source
theorem set.mem_set_of {α : Type u} {a : α} {p : α → Prop} :
a ∈ {x : α | p x} ↔ p a
source
theorem has_mem.mem.out {α : Type u} {p : α → Prop} {a : α} (h : a ∈ {x : α | p x}) :
p a

If h : a ∈ {x | p x} then h.out : p x. These are definitionally equal, but this can nevertheless be useful for various reasons, e.g. to apply further projection notation or in an argument to simp.

source
theorem set.nmem_set_of_iff {α : Type u} {a : α} {p : α → Prop} :
a ∉ {x : α | p x} ↔ ¬p a
source
@[simp]
theorem set.set_of_mem_eq {α : Type u} {s : set α} :
{x : α | x ∈ s} = s
source
theorem set.set_of_set {α : Type u} {s : set α} :
set_of s = s
source
theorem set.set_of_app_iff {α : Type u} {p : α → Prop} {x : α} :
{x : α | p x} x ↔ p x
source
theorem set.mem_def {α : Type u} {a : α} {s : set α} :
a ∈ s ↔ s a
source
theorem set.set_of_bijective {α : Type u} :
function.bijective set_of
source
@[simp]
theorem set.set_of_subset_set_of {α : Type u} {p q : α → Prop} :
{a : α | p a} ⊆ {a : α | q a} ↔ ∀ (a : α), p a → q a
source
theorem set.set_of_and {α : Type u} {p q : α → Prop} :
{a : α | p a ∧ q a} = {a : α | p a} ∩ {a : α | q a}
source
theorem set.set_of_or {α : Type u} {p q : α → Prop} :
{a : α | p a ∨ q a} = {a : α | p a} ∪ {a : α | q a}

Subset and strict subset relations #

source
@[protected, instance]
def set.has_subset.subset.is_refl {α : Type u} :
is_refl (set α) has_subset.subset
source
@[protected, instance]
def set.has_subset.subset.is_trans {α : Type u} :
is_trans (set α) has_subset.subset
source
@[protected, instance]
def set.has_subset.subset.is_antisymm {α : Type u} :
is_antisymm (set α) has_subset.subset
source
@[protected, instance]
def set.has_ssubset.ssubset.is_irrefl {α : Type u} :
is_irrefl (set α) has_ssubset.ssubset
source
@[protected, instance]
def set.has_ssubset.ssubset.is_trans {α : Type u} :
is_trans (set α) has_ssubset.ssubset
source
@[protected, instance]
def set.has_ssubset.ssubset.is_asymm {α : Type u} :
is_asymm (set α) has_ssubset.ssubset
source
@[protected, instance]
def set.has_ssubset.ssubset.is_nonstrict_strict_order {α : Type u} :
is_nonstrict_strict_order (set α) has_subset.subset has_ssubset.ssubset
Equations
source
theorem set.subset_def {α : Type u} {s t : set α} :
s ⊆ t = ∀ (x : α), x ∈ s → x ∈ t
source
theorem set.ssubset_def {α : Type u} {s t : set α} :
s ⊂ t = (s ⊆ t ∧ ¬t ⊆ s)
source
@[refl]
theorem set.subset.refl {α : Type u} (a : set α) :
a ⊆ a
source
theorem set.subset.rfl {α : Type u} {s : set α} :
s ⊆ s
source
@[trans]
theorem set.subset.trans {α : Type u} {a b c : set α} (ab : a ⊆ b) (bc : b ⊆ c) :
a ⊆ c
source
@[trans]
theorem set.mem_of_eq_of_mem {α : Type u} {x y : α} {s : set α} (hx : x = y) (h : y ∈ s) :
x ∈ s
source
theorem set.subset.antisymm {α : Type u} {a b : set α} (h₁ : a ⊆ b) (h₂ : b ⊆ a) :
a = b
source
theorem set.subset.antisymm_iff {α : Type u} {a b : set α} :
a = b ↔ a ⊆ b ∧ b ⊆ a
source
theorem set.eq_of_subset_of_subset {α : Type u} {a b : set α} :
a ⊆ b → b ⊆ a → a = b
source
theorem set.mem_of_subset_of_mem {α : Type u} {s₁ s₂ : set α} {a : α} (h : s₁ ⊆ s₂) :
a ∈ s₁ → a ∈ s₂
source
theorem set.not_mem_subset {α : Type u} {a : α} {s t : set α} (h : s ⊆ t) :
a ∉ t → a ∉ s
source
theorem set.not_subset {α : Type u} {s t : set α} :
¬s ⊆ t ↔ ∃ (a : α) (H : a ∈ s), a ∉ t

Definition of strict subsets s ⊂ t and basic properties. #

source
@[protected]
theorem set.eq_or_ssubset_of_subset {α : Type u} {s t : set α} (h : s ⊆ t) :
s = t ∨ s ⊂ t
source
theorem set.exists_of_ssubset {α : Type u} {s t : set α} (h : s ⊂ t) :
∃ (x : α) (H : x ∈ t), x ∉ s
source
@[protected]
theorem set.ssubset_iff_subset_ne {α : Type u} {s t : set α} :
s ⊂ t ↔ s ⊆ t ∧ s ≠ t
source
theorem set.ssubset_iff_of_subset {α : Type u} {s t : set α} (h : s ⊆ t) :
s ⊂ t ↔ ∃ (x : α) (H : x ∈ t), x ∉ s
source
@[protected]
theorem set.ssubset_of_ssubset_of_subset {α : Type u} {s₁ s₂ s₃ : set α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) :
s₁ ⊂ s₃
source
@[protected]
theorem set.ssubset_of_subset_of_ssubset {α : Type u} {s₁ s₂ s₃ : set α} (hs₁s₂ : s₁ ⊆ s₂) (hs₂s₃ : s₂ ⊂ s₃) :
s₁ ⊂ s₃
source
theorem set.not_mem_empty {α : Type u} (x : α) :
x ∉ ∅
source
@[simp]
theorem set.not_not_mem {α : Type u} {a : α} {s : set α} :
¬a ∉ s ↔ a ∈ s

Non-empty sets #

source
@[protected]
def set.nonempty {α : Type u} (s : set α) :
Prop

The property s.nonempty expresses the fact that the set s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

Equations
source
@[simp]
theorem set.nonempty_coe_sort {α : Type u} {s : set α} :
nonempty ↥s ↔ s.nonempty
source
theorem set.nonempty.coe_sort {α : Type u} {s : set α} :
s.nonempty → nonempty ↥s

Alias of the reverse direction of set.nonempty_coe_sort.

source
theorem set.nonempty_def {α : Type u} {s : set α} :
s.nonempty ↔ ∃ (x : α), x ∈ s
source
theorem set.nonempty_of_mem {α : Type u} {s : set α} {x : α} (h : x ∈ s) :
s.nonempty
source
theorem set.nonempty.not_subset_empty {α : Type u} {s : set α} :
s.nonempty → ¬s ⊆ ∅
source
@[protected]
noncomputable def set.nonempty.some {α : Type u} {s : set α} (h : s.nonempty) :
α

Extract a witness from s.nonempty. 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
source
@[protected]
theorem set.nonempty.some_mem {α : Type u} {s : set α} (h : s.nonempty) :
h.some ∈ s
source
theorem set.nonempty.mono {α : Type u} {s t : set α} (ht : s ⊆ t) (hs : s.nonempty) :
t.nonempty
source
theorem set.nonempty_of_not_subset {α : Type u} {s t : set α} (h : ¬s ⊆ t) :
(s \ t).nonempty
source
theorem set.nonempty_of_ssubset {α : Type u} {s t : set α} (ht : s ⊂ t) :
(t \ s).nonempty
source
theorem set.nonempty.of_diff {α : Type u} {s t : set α} (h : (s \ t).nonempty) :
s.nonempty
source
theorem set.nonempty_of_ssubset' {α : Type u} {s t : set α} (ht : s ⊂ t) :
t.nonempty
source
theorem set.nonempty.inl {α : Type u} {s t : set α} (hs : s.nonempty) :
(s ∪ t).nonempty
source
theorem set.nonempty.inr {α : Type u} {s t : set α} (ht : t.nonempty) :
(s ∪ t).nonempty
source
@[simp]
theorem set.union_nonempty {α : Type u} {s t : set α} :
(s ∪ t).nonempty ↔ s.nonempty ∨ t.nonempty
source
theorem set.nonempty.left {α : Type u} {s t : set α} (h : (s ∩ t).nonempty) :
s.nonempty
source
theorem set.nonempty.right {α : Type u} {s t : set α} (h : (s ∩ t).nonempty) :
t.nonempty
source
theorem set.inter_nonempty {α : Type u} {s t : set α} :
(s ∩ t).nonempty ↔ ∃ (x : α), x ∈ s ∧ x ∈ t
source
theorem set.inter_nonempty_iff_exists_left {α : Type u} {s t : set α} :
(s ∩ t).nonempty ↔ ∃ (x : α) (H : x ∈ s), x ∈ t
source
theorem set.inter_nonempty_iff_exists_right {α : Type u} {s t : set α} :
(s ∩ t).nonempty ↔ ∃ (x : α) (H : x ∈ t), x ∈ s
source
theorem set.nonempty_iff_univ_nonempty {α : Type u} :
nonempty α ↔ set.univ.nonempty
source
@[simp]
theorem set.univ_nonempty {α : Type u} [h : nonempty α] :
set.univ.nonempty
source
theorem set.nonempty.to_subtype {α : Type u} {s : set α} :
s.nonempty → nonempty ↥s
source
theorem set.nonempty.to_type {α : Type u} {s : set α} :
s.nonempty → nonempty α
source
@[protected, instance]
def set.univ.nonempty {α : Type u} [nonempty α] :
nonempty ↥set.univ
source
theorem set.nonempty_of_nonempty_subtype {α : Type u} {s : set α} [nonempty ↥s] :
s.nonempty

Lemmas about the empty set #

source
theorem set.empty_def {α : Type u} :
∅ = {x : α | false}
source
@[simp]
theorem set.mem_empty_iff_false {α : Type u} (x : α) :
x ∈ ∅ ↔ false
source
@[simp]
theorem set.set_of_false {α : Type u} :
{a : α | false} = ∅
source
@[simp]
theorem set.empty_subset {α : Type u} (s : set α) :
∅ ⊆ s
source
theorem set.subset_empty_iff {α : Type u} {s : set α} :
s ⊆ ∅ ↔ s = ∅
source
theorem set.eq_empty_iff_forall_not_mem {α : Type u} {s : set α} :
s = ∅ ↔ ∀ (x : α), x ∉ s
source
theorem set.eq_empty_of_forall_not_mem {α : Type u} {s : set α} (h : ∀ (x : α), x ∉ s) :
s = ∅
source
theorem set.eq_empty_of_subset_empty {α : Type u} {s : set α} :
s ⊆ ∅ → s = ∅
source
theorem set.eq_empty_of_is_empty {α : Type u} [is_empty α] (s : set α) :
s = ∅
source
@[protected, instance]
def set.unique_empty {α : Type u} [is_empty α] :
unique (set α)

There is exactly one set of a type that is empty.

Equations
source
theorem set.not_nonempty_iff_eq_empty {α : Type u} {s : set α} :
¬s.nonempty ↔ s = ∅

See also set.nonempty_iff_ne_empty.

source
theorem set.nonempty_iff_ne_empty {α : Type u} {s : set α} :
s.nonempty ↔ s ≠ ∅

See also set.not_nonempty_iff_eq_empty.

source
theorem set.nonempty.ne_empty {α : Type u} {s : set α} :
s.nonempty → s ≠ ∅

Alias of the forward direction of set.nonempty_iff_ne_empty.

source
@[simp]
theorem set.not_nonempty_empty {α : Type u} :
¬∅.nonempty
source
@[simp]
theorem set.is_empty_coe_sort {α : Type u} {s : set α} :
is_empty ↥s ↔ s = ∅
source
theorem set.eq_empty_or_nonempty {α : Type u} (s : set α) :
s = ∅ ∨ s.nonempty
source
theorem set.subset_eq_empty {α : Type u} {s t : set α} (h : t ⊆ s) (e : s = ∅) :
t = ∅
source
theorem set.ball_empty_iff {α : Type u} {p : α → Prop} :
(∀ (x : α), x ∈ ∅ → p x) ↔ true
source
@[protected, instance]
def set.has_emptyc.emptyc.is_empty (α : Type u) :
is_empty ↥∅
source
@[simp]
theorem set.empty_ssubset {α : Type u} {s : set α} :
∅ ⊂ s ↔ s.nonempty
source
theorem set.nonempty.empty_ssubset {α : Type u} {s : set α} :
s.nonempty → ∅ ⊂ s

Alias of the reverse direction of set.empty_ssubset.

Universal set. #

In Lean @univ α (or univ : set α) is the set that contains all elements of type α. Mathematically it is the same as α but it has a different type.

source
@[simp]
theorem set.set_of_true {α : Type u} :
{x : α | true} = set.univ
source
@[simp]
theorem set.mem_univ {α : Type u} (x : α) :
x ∈ set.univ
source
@[simp]
theorem set.univ_eq_empty_iff {α : Type u} :
set.univ = ∅ ↔ is_empty α
source
theorem set.empty_ne_univ {α : Type u} [nonempty α] :
∅ ≠ set.univ
source
@[simp]
theorem set.subset_univ {α : Type u} (s : set α) :
s ⊆ set.univ
source
theorem set.univ_subset_iff {α : Type u} {s : set α} :
set.univ ⊆ s ↔ s = set.univ
source
theorem set.eq_univ_of_univ_subset {α : Type u} {s : set α} :
set.univ ⊆ s → s = set.univ

Alias of the forward direction of set.univ_subset_iff.

source
theorem set.eq_univ_iff_forall {α : Type u} {s : set α} :
s = set.univ ↔ ∀ (x : α), x ∈ s
source
theorem set.eq_univ_of_forall {α : Type u} {s : set α} :
(∀ (x : α), x ∈ s) → s = set.univ
source
theorem set.nonempty.eq_univ {α : Type u} {s : set α} [subsingleton α] :
s.nonempty → s = set.univ
source
theorem set.eq_univ_of_subset {α : Type u} {s t : set α} (h : s ⊆ t) (hs : s = set.univ) :
t = set.univ
source
theorem set.exists_mem_of_nonempty (α : Type u_1) [nonempty α] :
∃ (x : α), x ∈ set.univ
source
theorem set.ne_univ_iff_exists_not_mem {α : Type u_1} (s : set α) :
s ≠ set.univ ↔ ∃ (a : α), a ∉ s
source
theorem set.not_subset_iff_exists_mem_not_mem {α : Type u_1} {s t : set α} :
¬s ⊆ t ↔ ∃ (x : α), x ∈ s ∧ x ∉ t
source
theorem set.univ_unique {α : Type u} [unique α] :
set.univ = {inhabited.default}
source
theorem set.ssubset_univ_iff {α : Type u} {s : set α} :
s ⊂ set.univ ↔ s ≠ set.univ
source
@[protected, instance]
def set.nontrivial_of_nonempty {α : Type u} [nonempty α] :
nontrivial (set α)

Lemmas about union #

source
theorem set.union_def {α : Type u} {s₁ s₂ : set α} :
s₁ ∪ s₂ = {a : α | a ∈ s₁ ∨ a ∈ s₂}
source
theorem set.mem_union_left {α : Type u} {x : α} {a : set α} (b : set α) :
x ∈ a → x ∈ a ∪ b
source
theorem set.mem_union_right {α : Type u} {x : α} {b : set α} (a : set α) :
x ∈ b → x ∈ a ∪ b
source
theorem set.mem_or_mem_of_mem_union {α : Type u} {x : α} {a b : set α} (H : x ∈ a ∪ b) :
x ∈ a ∨ x ∈ b
source
theorem set.mem_union.elim {α : Type u} {x : α} {a b : set α} {P : Prop} (H₁ : x ∈ a ∪ b) (H₂ : x ∈ a → P) (H₃ : x ∈ b → P) :
P
source
@[simp]
theorem set.mem_union {α : Type u} (x : α) (a b : set α) :
x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b
source
@[simp]
theorem set.union_self {α : Type u} (a : set α) :
a ∪ a = a
source
@[simp]
theorem set.union_empty {α : Type u} (a : set α) :
a ∪ ∅ = a
source
@[simp]
theorem set.empty_union {α : Type u} (a : set α) :
∅ ∪ a = a
source
theorem set.union_comm {α : Type u} (a b : set α) :
a ∪ b = b ∪ a
source
theorem set.union_assoc {α : Type u} (a b c : set α) :
a ∪ b ∪ c = a ∪ (b ∪ c)
source
@[protected, instance]
def set.union_is_assoc {α : Type u} :
is_associative (set α) has_union.union
source
@[protected, instance]
def set.union_is_comm {α : Type u} :
is_commutative (set α) has_union.union
source
theorem set.union_left_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃)
source
theorem set.union_right_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃ ∪ s₂
source
@[simp]
theorem set.union_eq_left_iff_subset {α : Type u} {s t : set α} :
s ∪ t = s ↔ t ⊆ s
source
@[simp]
theorem set.union_eq_right_iff_subset {α : Type u} {s t : set α} :
s ∪ t = t ↔ s ⊆ t
source
theorem set.union_eq_self_of_subset_left {α : Type u} {s t : set α} (h : s ⊆ t) :
s ∪ t = t
source
theorem set.union_eq_self_of_subset_right {α : Type u} {s t : set α} (h : t ⊆ s) :
s ∪ t = s
source
@[simp]
theorem set.subset_union_left {α : Type u} (s t : set α) :
s ⊆ s ∪ t
source
@[simp]
theorem set.subset_union_right {α : Type u} (s t : set α) :
t ⊆ s ∪ t
source
theorem set.union_subset {α : Type u} {s t r : set α} (sr : s ⊆ r) (tr : t ⊆ r) :
s ∪ t ⊆ r
source
@[simp]
theorem set.union_subset_iff {α : Type u} {s t u : set α} :
s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u
source
theorem set.union_subset_union {α : Type u} {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ s₂) (h₂ : t₁ ⊆ t₂) :
s₁ ∪ t₁ ⊆ s₂ ∪ t₂
source
theorem set.union_subset_union_left {α : Type u} {s₁ s₂ : set α} (t : set α) (h : s₁ ⊆ s₂) :
s₁ ∪ t ⊆ s₂ ∪ t
source
theorem set.union_subset_union_right {α : Type u} (s : set α) {t₁ t₂ : set α} (h : t₁ ⊆ t₂) :
s ∪ t₁ ⊆ s ∪ t₂
source
theorem set.subset_union_of_subset_left {α : Type u} {s t : set α} (h : s ⊆ t) (u : set α) :
s ⊆ t ∪ u
source
theorem set.subset_union_of_subset_right {α : Type u} {s u : set α} (h : s ⊆ u) (t : set α) :
s ⊆ t ∪ u
source
theorem set.union_congr_left {α : Type u} {s t u : set α} (ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) :
s ∪ t = s ⊔ u
source
theorem set.union_congr_right {α : Type u} {s t u : set α} (hs : s ⊆ t ∪ u) (ht : t ⊆ s ∪ u) :
s ∪ u = t ∪ u
source
theorem set.union_eq_union_iff_left {α : Type u} {s t u : set α} :
s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t
source
theorem set.union_eq_union_iff_right {α : Type u} {s t u : set α} :
s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u
source
@[simp]
theorem set.union_empty_iff {α : Type u} {s t : set α} :
s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
source
@[simp]
theorem set.union_univ {α : Type u} {s : set α} :
s ∪ set.univ = set.univ
source
@[simp]
theorem set.univ_union {α : Type u} {s : set α} :
set.univ ∪ s = set.univ

Lemmas about intersection #

source
theorem set.inter_def {α : Type u} {s₁ s₂ : set α} :
s₁ ∩ s₂ = {a : α | a ∈ s₁ ∧ a ∈ s₂}
source
@[simp]
theorem set.mem_inter_iff {α : Type u} (x : α) (a b : set α) :
x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b
source
theorem set.mem_inter {α : Type u} {x : α} {a b : set α} (ha : x ∈ a) (hb : x ∈ b) :
x ∈ a ∩ b
source
theorem set.mem_of_mem_inter_left {α : Type u} {x : α} {a b : set α} (h : x ∈ a ∩ b) :
x ∈ a
source
theorem set.mem_of_mem_inter_right {α : Type u} {x : α} {a b : set α} (h : x ∈ a ∩ b) :
x ∈ b
source
@[simp]
theorem set.inter_self {α : Type u} (a : set α) :
a ∩ a = a
source
@[simp]
theorem set.inter_empty {α : Type u} (a : set α) :
a ∩ ∅ = ∅
source
@[simp]
theorem set.empty_inter {α : Type u} (a : set α) :
∅ ∩ a = ∅
source
theorem set.inter_comm {α : Type u} (a b : set α) :
a ∩ b = b ∩ a
source
theorem set.inter_assoc {α : Type u} (a b c : set α) :
a ∩ b ∩ c = a ∩ (b ∩ c)
source
@[protected, instance]
def set.inter_is_assoc {α : Type u} :
is_associative (set α) has_inter.inter
source
@[protected, instance]
def set.inter_is_comm {α : Type u} :
is_commutative (set α) has_inter.inter
source
theorem set.inter_left_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)
source
theorem set.inter_right_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂
source
@[simp]
theorem set.inter_subset_left {α : Type u} (s t : set α) :
s ∩ t ⊆ s
source
@[simp]
theorem set.inter_subset_right {α : Type u} (s t : set α) :
s ∩ t ⊆ t
source
theorem set.subset_inter {α : Type u} {s t r : set α} (rs : r ⊆ s) (rt : r ⊆ t) :
r ⊆ s ∩ t
source
@[simp]
theorem set.subset_inter_iff {α : Type u} {s t r : set α} :
r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t
source
@[simp]
theorem set.inter_eq_left_iff_subset {α : Type u} {s t : set α} :
s ∩ t = s ↔ s ⊆ t
source
@[simp]
theorem set.inter_eq_right_iff_subset {α : Type u} {s t : set α} :
s ∩ t = t ↔ t ⊆ s
source
theorem set.inter_eq_self_of_subset_left {α : Type u} {s t : set α} :
s ⊆ t → s ∩ t = s
source
theorem set.inter_eq_self_of_subset_right {α : Type u} {s t : set α} :
t ⊆ s → s ∩ t = t
source
theorem set.inter_congr_left {α : Type u} {s t u : set α} (ht : s ∩ u ⊆ t) (hu : s ∩ t ⊆ u) :
s ∩ t = s ∩ u
source
theorem set.inter_congr_right {α : Type u} {s t u : set α} (hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) :
s ∩ u = t ∩ u
source
theorem set.inter_eq_inter_iff_left {α : Type u} {s t u : set α} :
s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u
source
theorem set.inter_eq_inter_iff_right {α : Type u} {s t u : set α} :
s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t
source
@[simp]
theorem set.inter_univ {α : Type u} (a : set α) :
a ∩ set.univ = a
source
@[simp]
theorem set.univ_inter {α : Type u} (a : set α) :
set.univ ∩ a = a
source
theorem set.inter_subset_inter {α : Type u} {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) :
s₁ ∩ s₂ ⊆ t₁ ∩ t₂
source
theorem set.inter_subset_inter_left {α : Type u} {s t : set α} (u : set α) (H : s ⊆ t) :
s ∩ u ⊆ t ∩ u
source
theorem set.inter_subset_inter_right {α : Type u} {s t : set α} (u : set α) (H : s ⊆ t) :
u ∩ s ⊆ u ∩ t
source
theorem set.union_inter_cancel_left {α : Type u} {s t : set α} :
(s ∪ t) ∩ s = s
source
theorem set.union_inter_cancel_right {α : Type u} {s t : set α} :
(s ∪ t) ∩ t = t
source
theorem set.inter_set_of_eq_sep {α : Type u} (s : set α) (p : α → Prop) :
s ∩ {a : α | p a} = {a ∈ s | p a}
source
theorem set.set_of_inter_eq_sep {α : Type u} (p : α → Prop) (s : set α) :
{a : α | p a} ∩ s = {a ∈ s | p a}

Distributivity laws #

source
theorem set.inter_distrib_left {α : Type u} (s t u : set α) :
s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
source
theorem set.inter_union_distrib_left {α : Type u} {s t u : set α} :
s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
source
theorem set.inter_distrib_right {α : Type u} (s t u : set α) :
(s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
source
theorem set.union_inter_distrib_right {α : Type u} {s t u : set α} :
(s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
source
theorem set.union_distrib_left {α : Type u} (s t u : set α) :
s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
source
theorem set.union_inter_distrib_left {α : Type u} {s t u : set α} :
s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
source
theorem set.union_distrib_right {α : Type u} (s t u : set α) :
s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)
source
theorem set.inter_union_distrib_right {α : Type u} {s t u : set α} :
s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)
source
theorem set.union_union_distrib_left {α : Type u} (s t u : set α) :
s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)
source
theorem set.union_union_distrib_right {α : Type u} (s t u : set α) :
s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)
source
theorem set.inter_inter_distrib_left {α : Type u} (s t u : set α) :
s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)
source
theorem set.inter_inter_distrib_right {α : Type u} (s t u : set α) :
s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)
source
theorem set.union_union_union_comm {α : Type u} (s t u v : set α) :
s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)
source
theorem set.inter_inter_inter_comm {α : Type u} (s t u v : set α) :
s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)

Lemmas about insert #

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

source
theorem set.insert_def {α : Type u} (x : α) (s : set α) :
has_insert.insert x s = {y : α | y = x ∨ y ∈ s}
source
@[simp]
theorem set.subset_insert {α : Type u} (x : α) (s : set α) :
s ⊆ has_insert.insert x s
source
theorem set.mem_insert {α : Type u} (x : α) (s : set α) :
x ∈ has_insert.insert x s
source
theorem set.mem_insert_of_mem {α : Type u} {x : α} {s : set α} (y : α) :
x ∈ s → x ∈ has_insert.insert y s
source
theorem set.eq_or_mem_of_mem_insert {α : Type u} {x a : α} {s : set α} :
x ∈ has_insert.insert a s → x = a ∨ x ∈ s
source
theorem set.mem_of_mem_insert_of_ne {α : Type u} {a b : α} {s : set α} :
b ∈ has_insert.insert a s → b ≠ a → b ∈ s
source
theorem set.eq_of_not_mem_of_mem_insert {α : Type u} {a b : α} {s : set α} :
b ∈ has_insert.insert a s → b ∉ s → b = a
source
@[simp]
theorem set.mem_insert_iff {α : Type u} {x a : α} {s : set α} :
x ∈ has_insert.insert a s ↔ x = a ∨ x ∈ s
source
@[simp]
theorem set.insert_eq_of_mem {α : Type u} {a : α} {s : set α} (h : a ∈ s) :
has_insert.insert a s = s
source
theorem set.ne_insert_of_not_mem {α : Type u} {s : set α} (t : set α) {a : α} :
a ∉ s → s ≠ has_insert.insert a t
source
@[simp]
theorem set.insert_eq_self {α : Type u} {a : α} {s : set α} :
has_insert.insert a s = s ↔ a ∈ s
source
theorem set.insert_ne_self {α : Type u} {a : α} {s : set α} :
has_insert.insert a s ≠ s ↔ a ∉ s
source
theorem set.insert_subset {α : Type u} {a : α} {s t : set α} :
has_insert.insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
source
theorem set.insert_subset_insert {α : Type u} {a : α} {s t : set α} (h : s ⊆ t) :
has_insert.insert a s ⊆ has_insert.insert a t
source
theorem set.insert_subset_insert_iff {α : Type u} {a : α} {s t : set α} (ha : a ∉ s) :
has_insert.insert a s ⊆ has_insert.insert a t ↔ s ⊆ t
source
theorem set.subset_insert_iff_of_not_mem {α : Type u} {a : α} {s t : set α} (ha : a ∉ s) :
s ⊆ has_insert.insert a t ↔ s ⊆ t
source
theorem set.ssubset_iff_insert {α : Type u} {s t : set α} :
s ⊂ t ↔ ∃ (a : α) (H : a ∉ s), has_insert.insert a s ⊆ t
source
theorem set.ssubset_insert {α : Type u} {s : set α} {a : α} (h : a ∉ s) :
s ⊂ has_insert.insert a s
source
theorem set.insert_comm {α : Type u} (a b : α) (s : set α) :
has_insert.insert a (has_insert.insert b s) = has_insert.insert b (has_insert.insert a s)
source
@[simp]
theorem set.insert_idem {α : Type u} (a : α) (s : set α) :
has_insert.insert a (has_insert.insert a s) = has_insert.insert a s
source
theorem set.insert_union {α : Type u} {a : α} {s t : set α} :
has_insert.insert a s ∪ t = has_insert.insert a (s ∪ t)
source
@[simp]
theorem set.union_insert {α : Type u} {a : α} {s t : set α} :
s ∪ has_insert.insert a t = has_insert.insert a (s ∪ t)
source
@[simp]
theorem set.insert_nonempty {α : Type u} (a : α) (s : set α) :
(has_insert.insert a s).nonempty
source
@[protected, instance]
def set.has_insert.insert.nonempty {α : Type u} (a : α) (s : set α) :
nonempty ↥(has_insert.insert a s)
source
theorem set.insert_inter_distrib {α : Type u} (a : α) (s t : set α) :
has_insert.insert a (s ∩ t) = has_insert.insert a s ∩ has_insert.insert a t
source
theorem set.insert_union_distrib {α : Type u} (a : α) (s t : set α) :
has_insert.insert a (s ∪ t) = has_insert.insert a s ∪ has_insert.insert a t
source
theorem set.insert_inj {α : Type u} {a b : α} {s : set α} (ha : a ∉ s) :
has_insert.insert a s = has_insert.insert b s ↔ a = b
source
theorem set.forall_of_forall_insert {α : Type u} {P : α → Prop} {a : α} {s : set α} (H : ∀ (x : α), x ∈ has_insert.insert a s → P x) (x : α) (h : x ∈ s) :
P x
source
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
source
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
source
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

Lemmas about singletons #

source
theorem set.singleton_def {α : Type u} (a : α) :
{a} = {a}
source
@[simp]
theorem set.mem_singleton_iff {α : Type u} {a b : α} :
a ∈ {b} ↔ a = b
source
@[simp]
theorem set.set_of_eq_eq_singleton {α : Type u} {a : α} :
{n : α | n = a} = {a}
source
@[simp]
theorem set.set_of_eq_eq_singleton' {α : Type u} {a : α} :
{x : α | a = x} = {a}
source
@[simp]
theorem set.mem_singleton {α : Type u} (a : α) :
a ∈ {a}
source
theorem set.eq_of_mem_singleton {α : Type u} {x y : α} (h : x ∈ {y}) :
x = y
source
@[simp]
theorem set.singleton_eq_singleton_iff {α : Type u} {x y : α} :
{x} = {y} ↔ x = y
source
theorem set.singleton_injective {α : Type u} :
function.injective has_singleton.singleton
source
theorem set.mem_singleton_of_eq {α : Type u} {x y : α} (H : x = y) :
x ∈ {y}
source
theorem set.insert_eq {α : Type u} (x : α) (s : set α) :
has_insert.insert x s = {x} ∪ s
source
@[simp]
theorem set.singleton_nonempty {α : Type u} (a : α) :
{a}.nonempty
source
@[simp]
theorem set.singleton_ne_empty {α : Type u} (a : α) :
{a} ≠ ∅
source
@[simp]
theorem set.empty_ssubset_singleton {α : Type u} {a : α} :
∅ ⊂ {a}
source
@[simp]
theorem set.singleton_subset_iff {α : Type u} {a : α} {s : set α} :
{a} ⊆ s ↔ a ∈ s
source
theorem set.singleton_subset_singleton {α : Type u} {a b : α} :
{a} ⊆ {b} ↔ a = b
source
theorem set.set_compr_eq_eq_singleton {α : Type u} {a : α} :
{b : α | b = a} = {a}
source
@[simp]
theorem set.singleton_union {α : Type u} {a : α} {s : set α} :
{a} ∪ s = has_insert.insert a s
source
@[simp]
theorem set.union_singleton {α : Type u} {a : α} {s : set α} :
s ∪ {a} = has_insert.insert a s
source
@[simp]
theorem set.singleton_inter_nonempty {α : Type u} {a : α} {s : set α} :
({a} ∩ s).nonempty ↔ a ∈ s
source
@[simp]
theorem set.inter_singleton_nonempty {α : Type u} {a : α} {s : set α} :
(s ∩ {a}).nonempty ↔ a ∈ s
source
@[simp]
theorem set.singleton_inter_eq_empty {α : Type u} {a : α} {s : set α} :
{a} ∩ s = ∅ ↔ a ∉ s
source
@[simp]
theorem set.inter_singleton_eq_empty {α : Type u} {a : α} {s : set α} :
s ∩ {a} = ∅ ↔ a ∉ s
source
theorem set.nmem_singleton_empty {α : Type u} {s : set α} :
s ∉ {∅} ↔ s.nonempty
source
@[protected, instance]
def set.unique_singleton {α : Type u} (a : α) :
unique ↥{a}
Equations
source
theorem set.eq_singleton_iff_unique_mem {α : Type u} {a : α} {s : set α} :
s = {a} ↔ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
source
theorem set.eq_singleton_iff_nonempty_unique_mem {α : Type u} {a : α} {s : set α} :
s = {a} ↔ s.nonempty ∧ ∀ (x : α), x ∈ s → x = a
source
@[simp]
theorem set.default_coe_singleton {α : Type u} (x : α) :
inhabited.default = ⟨x, _⟩

Lemmas about pairs #

source
@[simp]
theorem set.pair_eq_singleton {α : Type u} (a : α) :
{a, a} = {a}
source
theorem set.pair_comm {α : Type u} (a b : α) :
{a, b} = {b, a}
source
theorem set.pair_eq_pair_iff {α : Type u} {x y z w : α} :
{x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Lemmas about sets defined as {x ∈ s | p x}. #

source
theorem set.mem_sep {α : Type u} {s : set α} {p : α → Prop} {x : α} (xs : x ∈ s) (px : p x) :
x ∈ {x ∈ s | p x}
source
@[simp]
theorem set.sep_mem_eq {α : Type u} {s t : set α} :
{x ∈ s | x ∈ t} = s ∩ t
source
@[simp]
theorem set.mem_sep_iff {α : Type u} {s : set α} {p : α → Prop} {x : α} :
x ∈ {x ∈ s | p x} ↔ x ∈ s ∧ p x
source
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)
source
theorem set.sep_eq_of_subset {α : Type u} {s t : set α} (h : s ⊆ t) :
{x ∈ t | x ∈ s} = s
source
@[simp]
theorem set.sep_subset {α : Type u} (s : set α) (p : α → Prop) :
{x ∈ s | p x} ⊆ s
source
@[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
source
@[simp]
theorem set.sep_eq_empty_iff_mem_false {α : Type u} {s : set α} {p : α → Prop} :
{x ∈ s | p x} = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
source
@[simp]
theorem set.sep_true {α : Type u} {s : set α} :
{x ∈ s | true} = s
source
@[simp]
theorem set.sep_false {α : Type u} {s : set α} :
{x ∈ s | false} = ∅
source
@[simp]
theorem set.sep_empty {α : Type u} (p : α → Prop) :
{x ∈ ∅ | p x} = ∅
source
@[simp]
theorem set.sep_univ {α : Type u} {p : α → Prop} :
{x ∈ set.univ | p x} = {x : α | p x}
source
@[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}
source
@[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}
source
@[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}
source
@[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}
source
@[simp]
theorem set.sep_set_of {α : Type u} {p q : α → Prop} :
{x ∈ {y : α | p y} | q x} = {x : α | p x ∧ q x}
source
@[simp]
theorem set.subset_singleton_iff {α : Type u_1} {s : set α} {x : α} :
s ⊆ {x} ↔ ∀ (y : α), y ∈ s → y = x
source
theorem set.subset_singleton_iff_eq {α : Type u} {s : set α} {x : α} :
s ⊆ {x} ↔ s = ∅ ∨ s = {x}
source
theorem set.nonempty.subset_singleton_iff {α : Type u} {a : α} {s : set α} (h : s.nonempty) :
s ⊆ {a} ↔ s = {a}
source
theorem set.ssubset_singleton_iff {α : Type u} {s : set α} {x : α} :
s ⊂ {x} ↔ s = ∅
source
theorem set.eq_empty_of_ssubset_singleton {α : Type u} {s : set α} {x : α} (hs : s ⊂ {x}) :
s = ∅

Disjointness #

source
@[protected]
theorem set.disjoint_iff {α : Type u} {s t : set α} :
disjoint s t ↔ s ∩ t ⊆ ∅
source
theorem set.disjoint_iff_inter_eq_empty {α : Type u} {s t : set α} :
disjoint s t ↔ s ∩ t = ∅
source
theorem disjoint.inter_eq {α : Type u} {s t : set α} :
disjoint s t → s ∩ t = ∅
source
theorem set.disjoint_left {α : Type u} {s t : set α} :
disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
source
theorem set.disjoint_right {α : Type u} {s t : set α} :
disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
source
theorem set.not_disjoint_iff {α : Type u} {s t : set α} :
¬disjoint s t ↔ ∃ (x : α), x ∈ s ∧ x ∈ t
source
theorem set.not_disjoint_iff_nonempty_inter {α : Type u} {s t : set α} :
¬disjoint s t ↔ (s ∩ t).nonempty
source
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.

source
theorem set.disjoint_or_nonempty_inter {α : Type u} (s t : set α) :
disjoint s t ∨ (s ∩ t).nonempty
source
theorem set.disjoint_iff_forall_ne {α : Type u} {s t : set α} :
disjoint s t ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x ≠ y
source
theorem disjoint.ne_of_mem {α : Type u} {s t : set α} (h : disjoint s t) {x y : α} (hx : x ∈ s) (hy : y ∈ t) :
x ≠ y
source
theorem set.disjoint_of_subset_left {α : Type u} {s₁ s₂ t : set α} (hs : s₁ ⊆ s₂) (h : disjoint s₂ t) :
disjoint s₁ t
source
theorem set.disjoint_of_subset_right {α : Type u} {s t₁ t₂ : set α} (ht : t₁ ⊆ t₂) (h : disjoint s t₂) :
disjoint s t₁
source
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₁
source
@[simp]
theorem set.disjoint_union_left {α : Type u} {s t u : set α} :
disjoint (s ∪ t) u ↔ disjoint s u ∧ disjoint t u
source
@[simp]
theorem set.disjoint_union_right {α : Type u} {s t u : set α} :
disjoint s (t ∪ u) ↔ disjoint s t ∧ disjoint s u
source
@[simp]
theorem set.disjoint_empty {α : Type u} (s : set α) :
disjoint s ∅
source
@[simp]
theorem set.empty_disjoint {α : Type u} (s : set α) :
disjoint ∅ s
source
@[simp]
theorem set.univ_disjoint {α : Type u} {s : set α} :
disjoint set.univ s ↔ s = ∅
source
@[simp]
theorem set.disjoint_univ {α : Type u} {s : set α} :
disjoint s set.univ ↔ s = ∅
source
theorem set.disjoint_sdiff_left {α : Type u} {s t : set α} :
disjoint (t \ s) s
source
theorem set.disjoint_sdiff_right {α : Type u} {s t : set α} :
disjoint s (t \ s)
source
theorem set.diff_union_diff_cancel {α : Type u} {s t u : set α} (hts : t ⊆ s) (hut : u ⊆ t) :
s \ t ∪ t \ u = s \ u
source
theorem set.diff_diff_eq_sdiff_union {α : Type u} {s t u : set α} (h : u ⊆ s) :
s \ (t \ u) = s \ t ∪ u
source
@[simp]
theorem set.disjoint_singleton_left {α : Type u} {a : α} {s : set α} :
disjoint {a} s ↔ a ∉ s
source
@[simp]
theorem set.disjoint_singleton_right {α : Type u} {a : α} {s : set α} :
disjoint s {a} ↔ a ∉ s
source
@[simp]
theorem set.disjoint_singleton {α : Type u} {a b : α} :
disjoint {a} {b} ↔ a ≠ b
source
theorem set.subset_diff {α : Type u} {s t u : set α} :
s ⊆ t \ u ↔ s ⊆ t ∧ disjoint s u
source
theorem set.inter_diff_distrib_left {α : Type u} (s t u : set α) :
s ∩ (t \ u) = s ∩ t \ (s ∩ u)
source
theorem set.inter_diff_distrib_right {α : Type u} (s t u : set α) :
s \ t ∩ u = s ∩ u \ (t ∩ u)

Lemmas about complement #

source
theorem set.compl_def {α : Type u} (s : set α) :
sᶜ = {x : α | x ∉ s}
source
theorem set.mem_compl {α : Type u} {s : set α} {x : α} (h : x ∉ s) :
x ∈ sᶜ
source
theorem set.compl_set_of {α : Type u_1} (p : α → Prop) :
{a : α | p a}ᶜ = {a : α | ¬p a}
source
theorem set.not_mem_of_mem_compl {α : Type u} {s : set α} {x : α} (h : x ∈ sᶜ) :
x ∉ s
source
@[simp]
theorem set.mem_compl_iff {α : Type u} (s : set α) (x : α) :
x ∈ sᶜ ↔ x ∉ s
source
theorem set.not_mem_compl_iff {α : Type u} {s : set α} {x : α} :
x ∉ sᶜ ↔ x ∈ s
source
@[simp]
theorem set.inter_compl_self {α : Type u} (s : set α) :
s ∩ sᶜ = ∅
source
@[simp]
theorem set.compl_inter_self {α : Type u} (s : set α) :
sᶜ ∩ s = ∅
source
@[simp]
theorem set.compl_empty {α : Type u} :
∅ᶜ = set.univ
source
@[simp]
theorem set.compl_union {α : Type u} (s t : set α) :
(s ∪ t)ᶜ = sᶜ ∩ tᶜ
source
theorem set.compl_inter {α : Type u} (s t : set α) :
(s ∩ t)ᶜ = sᶜ ∪ tᶜ
source
@[simp]
theorem set.compl_univ {α : Type u} :
set.univᶜ = ∅
source
@[simp]
theorem set.compl_empty_iff {α : Type u} {s : set α} :
sᶜ = ∅ ↔ s = set.univ
source
@[simp]
theorem set.compl_univ_iff {α : Type u} {s : set α} :
sᶜ = set.univ ↔ s = ∅
source
theorem set.compl_ne_univ {α : Type u} {s : set α} :
sᶜ ≠ set.univ ↔ s.nonempty
source
theorem set.nonempty_compl {α : Type u} {s : set α} :
sᶜ.nonempty ↔ s ≠ set.univ
source
theorem set.mem_compl_singleton_iff {α : Type u} {a x : α} :
x ∈ {a}ᶜ ↔ x ≠ a
source
theorem set.compl_singleton_eq {α : Type u} (a : α) :
{a}ᶜ = {x : α | x ≠ a}
source
@[simp]
theorem set.compl_ne_eq_singleton {α : Type u} (a : α) :
{x : α | x ≠ a}ᶜ = {a}
source
theorem set.union_eq_compl_compl_inter_compl {α : Type u} (s t : set α) :
s ∪ t = (sᶜ ∩ tᶜ)ᶜ
source
theorem set.inter_eq_compl_compl_union_compl {α : Type u} (s t : set α) :
s ∩ t = (sᶜ ∪ tᶜ)ᶜ
source
@[simp]
theorem set.union_compl_self {α : Type u} (s : set α) :
s ∪ sᶜ = set.univ
source
@[simp]
theorem set.compl_union_self {α : Type u} (s : set α) :
sᶜ ∪ s = set.univ
source
theorem set.compl_subset_comm {α : Type u} {s t : set α} :
sᶜ ⊆ t ↔ tᶜ ⊆ s
source
theorem set.subset_compl_comm {α : Type u} {s t : set α} :
s ⊆ tᶜ ↔ t ⊆ sᶜ
source
@[simp]
theorem set.compl_subset_compl {α : Type u} {s t : set α} :
sᶜ ⊆ tᶜ ↔ t ⊆ s
source
theorem set.subset_compl_iff_disjoint_left {α : Type u} {s t : set α} :
s ⊆ tᶜ ↔ disjoint t s
source
theorem set.subset_compl_iff_disjoint_right {α : Type u} {s t : set α} :
s ⊆ tᶜ ↔ disjoint s t
source
theorem set.disjoint_compl_left_iff_subset {α : Type u} {s t : set α} :
disjoint sᶜ t ↔ t ⊆ s
source
theorem set.disjoint_compl_right_iff_subset {α : Type u} {s t : set α} :
disjoint s tᶜ ↔ s ⊆ t
source
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.

source
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.

source
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.

source
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.

source
theorem set.subset_union_compl_iff_inter_subset {α : Type u} {s t u : set α} :
s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t
source
theorem set.compl_subset_iff_union {α : Type u} {s t : set α} :
sᶜ ⊆ t ↔ s ∪ t = set.univ
source
@[simp]
theorem set.subset_compl_singleton_iff {α : Type u} {a : α} {s : set α} :
s ⊆ {a}ᶜ ↔ a ∉ s
source
theorem set.inter_subset {α : Type u} (a b c : set α) :
a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c
source
theorem set.inter_compl_nonempty_iff {α : Type u} {s t : set α} :
(s ∩ tᶜ).nonempty ↔ ¬s ⊆ t

Lemmas about set difference #

source
theorem set.diff_eq {α : Type u} (s t : set α) :
s \ t = s ∩ tᶜ
source
@[simp]
theorem set.mem_diff {α : Type u} {s t : set α} (x : α) :
x ∈ s \ t ↔ x ∈ s ∧ x ∉ t
source
theorem set.mem_diff_of_mem {α : Type u} {s t : set α} {x : α} (h1 : x ∈ s) (h2 : x ∉ t) :
x ∈ s \ t
source
theorem set.not_mem_diff_of_mem {α : Type u} {s t : set α} {x : α} (hx : x ∈ t) :
x ∉ s \ t
source
theorem set.mem_of_mem_diff {α : Type u} {s t : set α} {x : α} (h : x ∈ s \ t) :
x ∈ s
source
theorem set.not_mem_of_mem_diff {α : Type u} {s t : set α} {x : α} (h : x ∈ s \ t) :
x ∉ t
source
theorem set.diff_eq_compl_inter {α : Type u} {s t : set α} :
s \ t = tᶜ ∩ s
source
theorem set.nonempty_diff {α : Type u} {s t : set α} :
(s \ t).nonempty ↔ ¬s ⊆ t
source
theorem set.diff_subset {α : Type u} (s t : set α) :
s \ t ⊆ s
source
theorem set.union_diff_cancel' {α : Type u} {s t u : set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) :
t ∪ u \ s = u
source
theorem set.union_diff_cancel {α : Type u} {s t : set α} (h : s ⊆ t) :
s ∪ t \ s = t
source
theorem set.union_diff_cancel_left {α : Type u} {s t : set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ s = t
source
theorem set.union_diff_cancel_right {α : Type u} {s t : set α} (h : s ∩ t ⊆ ∅) :
(s ∪ t) \ t = s
source
@[simp]
theorem set.union_diff_left {α : Type u} {s t : set α} :
(s ∪ t) \ s = t \ s
source
@[simp]
theorem set.union_diff_right {α : Type u} {s t : set α} :
(s ∪ t) \ t = s \ t
source
theorem set.union_diff_distrib {α : Type u} {s t u : set α} :
(s ∪ t) \ u = s \ u ∪ t \ u
source
theorem set.inter_diff_assoc {α : Type u} (a b c : set α) :
a ∩ b \ c = a ∩ (b \ c)
source
@[simp]
theorem set.inter_diff_self {α : Type u} (a b : set α) :
a ∩ (b \ a) = ∅
source
@[simp]
theorem set.inter_union_diff {α : Type u} (s t : set α) :
s ∩ t ∪ s \ t = s
source
@[simp]
theorem set.diff_union_inter {α : Type u} (s t : set α) :
s \ t ∪ s ∩ t = s
source
@[simp]
theorem set.inter_union_compl {α : Type u} (s t : set α) :
s ∩ t ∪ s ∩ tᶜ = s
source
theorem set.diff_subset_diff {α : Type u} {s₁ s₂ t₁ t₂ : set α} :
s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂
source
theorem set.diff_subset_diff_left {α : Type u} {s₁ s₂ t : set α} (h : s₁ ⊆ s₂) :
s₁ \ t ⊆ s₂ \ t
source
theorem set.diff_subset_diff_right {α : Type u} {s t u : set α} (h : t ⊆ u) :
s \ u ⊆ s \ t
source
theorem set.compl_eq_univ_diff {α : Type u} (s : set α) :
sᶜ = set.univ \ s
source
@[simp]
theorem set.empty_diff {α : Type u} (s : set α) :
∅ \ s = ∅
source
theorem set.diff_eq_empty {α : Type u} {s t : set α} :
s \ t = ∅ ↔ s ⊆ t
source
@[simp]
theorem set.diff_empty {α : Type u} {s : set α} :
s \ ∅ = s
source
@[simp]
theorem set.diff_univ {α : Type u} (s : set α) :
s \ set.univ = ∅
source
theorem set.diff_diff {α : Type u} {s t u : set α} :
s \ t \ u = s \ (t ∪ u)
source
theorem set.diff_diff_comm {α : Type u} {s t u : set α} :
s \ t \ u = s \ u \ t
source
theorem set.diff_subset_iff {α : Type u} {s t u : set α} :
s \ t ⊆ u ↔ s ⊆ t ∪ u
source
theorem set.subset_diff_union {α : Type u} (s t : set α) :
s ⊆ s \ t ∪ t
source
theorem set.diff_union_of_subset {α : Type u} {s t : set α} (h : t ⊆ s) :
s \ t ∪ t = s
source
@[simp]
theorem set.diff_singleton_subset_iff {α : Type u} {x : α} {s t : set α} :
s \ {x} ⊆ t ↔ s ⊆ has_insert.insert x t
source
theorem set.subset_diff_singleton {α : Type u} {x : α} {s t : set α} (h : s ⊆ t) (hx : x ∉ s) :
s ⊆ t \ {x}
source
theorem set.subset_insert_diff_singleton {α : Type u} (x : α) (s : set α) :
s ⊆ has_insert.insert x (s \ {x})
source
theorem set.diff_subset_comm {α : Type u} {s t u : set α} :
s \ t ⊆ u ↔ s \ u ⊆ t
source
theorem set.diff_inter {α : Type u} {s t u : set α} :
s \ (t ∩ u) = s \ t ∪ s \ u
source
theorem set.diff_inter_diff {α : Type u} {s t u : set α} :
s \ t ∩ (s \ u) = s \ (t ∪ u)
source
theorem set.diff_compl {α : Type u} {s t : set α} :
s \ tᶜ = s ∩ t
source
theorem set.diff_diff_right {α : Type u} {s t u : set α} :
s \ (t \ u) = s \ t ∪ s ∩ u
source
@[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
source
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)
source
theorem set.insert_diff_self_of_not_mem {α : Type u} {a : α} {s : set α} (h : a ∉ s) :
has_insert.insert a s \ {a} = s
source
@[simp]
theorem set.insert_diff_eq_singleton {α : Type u} {a : α} {s : set α} (h : a ∉ s) :
has_insert.insert a s \ s = {a}
source
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)
source
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)
source
theorem set.inter_insert_of_not_mem {α : Type u} {a : α} {s t : set α} (h : a ∉ s) :
s ∩ has_insert.insert a t = s ∩ t
source
theorem set.insert_inter_of_not_mem {α : Type u} {a : α} {s t : set α} (h : a ∉ t) :
has_insert.insert a s ∩ t = s ∩ t
source
@[simp]
theorem set.union_diff_self {α : Type u} {s t : set α} :
s ∪ t \ s = s ∪ t
source
@[simp]
theorem set.diff_union_self {α : Type u} {s t : set α} :
s \ t ∪ t = s ∪ t
source
@[simp]
theorem set.diff_inter_self {α : Type u} {a b : set α} :
b \ a ∩ a = ∅
source
@[simp]
theorem set.diff_inter_self_eq_diff {α : Type u} {s t : set α} :
s \ (t ∩ s) = s \ t
source
@[simp]
theorem set.diff_self_inter {α : Type u} {s t : set α} :
s \ (s ∩ t) = s \ t
source
@[simp]
theorem set.diff_singleton_eq_self {α : Type u} {a : α} {s : set α} (h : a ∉ s) :
s \ {a} = s
source
@[simp]
theorem set.diff_singleton_ssubset {α : Type u} {s : set α} {a : α} :
s \ {a} ⊂ s ↔ a ∈ s
source
@[simp]
theorem set.insert_diff_singleton {α : Type u} {a : α} {s : set α} :
has_insert.insert a (s \ {a}) = has_insert.insert a s
source
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}
source
@[simp]
theorem set.diff_self {α : Type u} {s : set α} :
s \ s = ∅
source
theorem set.diff_diff_right_self {α : Type u} (s t : set α) :
s \ (s \ t) = s ∩ t
source
theorem set.diff_diff_cancel_left {α : Type u} {s t : set α} (h : s ⊆ t) :
t \ (t \ s) = s
source
theorem set.mem_diff_singleton {α : Type u} {x y : α} {s : set α} :
x ∈ s \ {y} ↔ x ∈ s ∧ x ≠ y
source
theorem set.mem_diff_singleton_empty {α : Type u} {s : set α} {t : set (set α)} :
s ∈ t \ {∅} ↔ s ∈ t ∧ s.nonempty
source
theorem set.union_eq_diff_union_diff_union_inter {α : Type u} (s t : set α) :
s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

Symmetric difference #

source
theorem set.mem_symm_diff {α : Type u} {a : α} {s t : set α} :
a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
source
@[protected]
theorem set.symm_diff_def {α : Type u} (s t : set α) :
s ∆ t = s \ t ∪ t \ s
source
theorem set.symm_diff_subset_union {α : Type u} {s t : set α} :
s ∆ t ⊆ s ∪ t
source
@[simp]
theorem set.symm_diff_eq_empty {α : Type u} {s t : set α} :
s ∆ t = ∅ ↔ s = t
source
@[simp]
theorem set.symm_diff_nonempty {α : Type u} {s t : set α} :
(s ∆ t).nonempty ↔ s ≠ t
source
theorem set.inter_symm_diff_distrib_left {α : Type u} (s t u : set α) :
s ∩ t ∆ u = (s ∩ t) ∆ (s ∩ u)
source
theorem set.inter_symm_diff_distrib_right {α : Type u} (s t u : set α) :
s ∆ t ∩ u = (s ∩ u) ∆ (t ∩ u)
source
theorem set.subset_symm_diff_union_symm_diff_left {α : Type u} {s t u : set α} (h : disjoint s t) :
u ⊆ s ∆ u ∪ t ∆ u
source
theorem set.subset_symm_diff_union_symm_diff_right {α : Type u} {s t u : set α} (h : disjoint t u) :
s ⊆ s ∆ t ∪ s ∆ u

Powerset #

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

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

Equations
source
theorem set.mem_powerset {α : Type u} {x s : set α} (h : x ⊆ s) :
x ∈ 𝒫s
source
theorem set.subset_of_mem_powerset {α : Type u} {x s : set α} (h : x ∈ 𝒫s) :
x ⊆ s
source
@[simp]
theorem set.mem_powerset_iff {α : Type u} (x s : set α) :
x ∈ 𝒫s ↔ x ⊆ s
source
theorem set.powerset_inter {α : Type u} (s t : set α) :
𝒫(s ∩ t) = 𝒫s ∩ 𝒫t
source
@[simp]
theorem set.powerset_mono {α : Type u} {s t : set α} :
𝒫s ⊆ 𝒫t ↔ s ⊆ t
source
theorem set.monotone_powerset {α : Type u} :
monotone set.powerset
source
@[simp]
theorem set.powerset_nonempty {α : Type u} {s : set α} :
(𝒫s).nonempty
source
@[simp]
theorem set.powerset_empty {α : Type u} :
𝒫∅ = {∅}
source
@[simp]
theorem set.powerset_univ {α : Type u} :
𝒫set.univ = set.univ
source
theorem set.powerset_singleton {α : Type u} (x : α) :
𝒫{x} = {∅, {x}}

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

Sets defined as an if-then-else #

source
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
source
@[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
source
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
source
@[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
source
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
source
@[simp]
theorem set.mem_ite_empty_right {α : Type u} (p : Prop) [decidable p] (t : set α) (x : α) :
x ∈ ite p t ∅ ↔ p ∧ x ∈ t
source
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
source
@[simp]
theorem set.mem_ite_empty_left {α : Type u} (p : Prop) [decidable p] (t : set α) (x : α) :
x ∈ ite p ∅ t ↔ ¬p ∧ x ∈ t

If-then-else for sets #

source
@[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
source
@[simp]
theorem set.ite_inter_self {α : Type u} (t s s' : set α) :
t.ite s s' ∩ t = s ∩ t
source
@[simp]
theorem set.ite_compl {α : Type u} (t s s' : set α) :
tᶜ.ite s s' = t.ite s' s
source
@[simp]
theorem set.ite_inter_compl_self {α : Type u} (t s s' : set α) :
t.ite s s' ∩ tᶜ = s' ∩ tᶜ
source
@[simp]
theorem set.ite_diff_self {α : Type u} (t s s' : set α) :
t.ite s s' \ t = s' \ t
source
@[simp]
theorem set.ite_same {α : Type u} (t s : set α) :
t.ite s s = s
source
@[simp]
theorem set.ite_left {α : Type u} (s t : set α) :
s.ite s t = s ∪ t
source
@[simp]
theorem set.ite_right {α : Type u} (s t : set α) :
s.ite t s = t ∩ s
source
@[simp]
theorem set.ite_empty {α : Type u} (s s' : set α) :
∅.ite s s' = s'
source
@[simp]
theorem set.ite_univ {α : Type u} (s s' : set α) :
set.univ.ite s s' = s
source
@[simp]
theorem set.ite_empty_left {α : Type u} (t s : set α) :
t.ite ∅ s = s \ t
source
@[simp]
theorem set.ite_empty_right {α : Type u} (t s : set α) :
t.ite s ∅ = s ∩ t
source
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₂'
source
theorem set.ite_subset_union {α : Type u} (t s s' : set α) :
t.ite s s' ⊆ s ∪ s'
source
theorem set.inter_subset_ite {α : Type u} (t s s' : set α) :
s ∩ s' ⊆ t.ite s s'
source
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₂'
source
theorem set.ite_inter {α : Type u} (t s₁ s₂ s : set α) :
t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s
source
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
source
theorem set.subset_ite {α : Type u} {t s s' u : set α} :
u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'

Subsingleton #

source
@[protected]
def set.subsingleton {α : Type u} (s : set α) :
Prop

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

Equations
source
theorem set.subsingleton.anti {α : Type u} {s t : set α} (ht : t.subsingleton) (hst : s ⊆ t) :
s.subsingleton
source
theorem set.subsingleton.eq_singleton_of_mem {α : Type u} {s : set α} (hs : s.subsingleton) {x : α} (hx : x ∈ s) :
s = {x}
source
@[simp]
theorem set.subsingleton_empty {α : Type u} :
∅.subsingleton
source
@[simp]
theorem set.subsingleton_singleton {α : Type u} {a : α} :
{a}.subsingleton
source
theorem set.subsingleton_of_subset_singleton {α : Type u} {a : α} {s : set α} (h : s ⊆ {a}) :
s.subsingleton
source
theorem set.subsingleton_of_forall_eq {α : Type u} {s : set α} (a : α) (h : ∀ (b : α), b ∈ s → b = a) :
s.subsingleton
source
theorem set.subsingleton_iff_singleton {α : Type u} {s : set α} {x : α} (hx : x ∈ s) :
s.subsingleton ↔ s = {x}
source
theorem set.subsingleton.eq_empty_or_singleton {α : Type u} {s : set α} (hs : s.subsingleton) :
s = ∅ ∨ ∃ (x : α), s = {x}
source
theorem set.subsingleton.induction_on {α : Type u} {s : set α} {p : set α → Prop} (hs : s.subsingleton) (he : p ∅) (h₁ : ∀ (x : α), p {x}) :
p s
source
theorem set.subsingleton_univ {α : Type u} [subsingleton α] :
set.univ.subsingleton
source
theorem set.subsingleton_of_univ_subsingleton {α : Type u} (h : set.univ.subsingleton) :
subsingleton α
source
@[simp]
theorem set.subsingleton_univ_iff {α : Type u} :
set.univ.subsingleton ↔ subsingleton α
source
theorem set.subsingleton_of_subsingleton {α : Type u} [subsingleton α] {s : set α} :
s.subsingleton
source
theorem set.subsingleton_is_top (α : Type u_1) [partial_order α] :
{x : α | is_top x}.subsingleton
source
theorem set.subsingleton_is_bot (α : Type u_1) [partial_order α] :
{x : α | is_bot x}.subsingleton
source
theorem set.exists_eq_singleton_iff_nonempty_subsingleton {α : Type u} {s : set α} :
(∃ (a : α), s = {a}) ↔ s.nonempty ∧ s.subsingleton
source
@[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.

source
theorem set.subsingleton.coe_sort {α : Type u} {s : set α} :
s.subsingleton → subsingleton ↥s
source
@[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.

Nontrivial #

source
@[protected]
def set.nontrivial {α : Type u} (s : set α) :
Prop

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

Equations
source
theorem set.nontrivial_of_mem_mem_ne {α : Type u} {s : set α} {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) :
s.nontrivial
source
@[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
source
@[protected]
theorem set.nontrivial.some_fst_mem {α : Type u} {s : set α} (hs : s.nontrivial) :
hs.some.fst ∈ s
source
@[protected]
theorem set.nontrivial.some_snd_mem {α : Type u} {s : set α} (hs : s.nontrivial) :
hs.some.snd ∈ s
source
@[protected]
theorem set.nontrivial.some_fst_ne_some_snd {α : Type u} {s : set α} (hs : s.nontrivial) :
hs.some.fst ≠ hs.some.snd
source
theorem set.nontrivial.mono {α : Type u} {s t : set α} (hs : s.nontrivial) (hst : s ⊆ t) :
t.nontrivial
source
theorem set.nontrivial_pair {α : Type u} {x y : α} (hxy : x ≠ y) :
{x, y}.nontrivial
source
theorem set.nontrivial_of_pair_subset {α : Type u} {s : set α} {x y : α} (hxy : x ≠ y) (h : {x, y} ⊆ s) :
s.nontrivial
source
theorem set.nontrivial.pair_subset {α : Type u} {s : set α} (hs : s.nontrivial) :
∃ (x y : α) (hab : x ≠ y), {x, y} ⊆ s
source
theorem set.nontrivial_iff_pair_subset {α : Type u} {s : set α} :
s.nontrivial ↔ ∃ (x y : α) (hxy : x ≠ y), {x, y} ⊆ s
source
theorem set.nontrivial_of_exists_ne {α : Type u} {s : set α} {x : α} (hx : x ∈ s) (h : ∃ (y : α) (H : y ∈ s), y ≠ x) :
s.nontrivial
source
theorem set.nontrivial.exists_ne {α : Type u} {s : set α} (hs : s.nontrivial) (z : α) :
∃ (x : α) (H : x ∈ s), x ≠ z
source
theorem set.nontrivial_iff_exists_ne {α : Type u} {s : set α} {x : α} (hx : x ∈ s) :
s.nontrivial ↔ ∃ (y : α) (H : y ∈ s), y ≠ x
source
theorem set.nontrivial_of_lt {α : Type u} {s : set α} [preorder α] {x y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : x < y) :
s.nontrivial
source
theorem set.nontrivial_of_exists_lt {α : Type u} {s : set α} [preorder α] (H : ∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x < y) :
s.nontrivial
source
theorem set.nontrivial.exists_lt {α : Type u} {s : set α} [linear_order α] (hs : s.nontrivial) :
∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x < y
source
theorem set.nontrivial_iff_exists_lt {α : Type u} {s : set α} [linear_order α] :
s.nontrivial ↔ ∃ (x : α) (H : x ∈ s) (y : α) (H : y ∈ s), x < y
source
@[protected]
theorem set.nontrivial.nonempty {α : Type u} {s : set α} (hs : s.nontrivial) :
s.nonempty
source
@[protected]
theorem set.nontrivial.ne_empty {α : Type u} {s : set α} (hs : s.nontrivial) :
s ≠ ∅
source
theorem set.nontrivial.not_subset_empty {α : Type u} {s : set α} (hs : s.nontrivial) :
¬s ⊆ ∅
source
@[simp]
theorem set.not_nontrivial_empty {α : Type u} :
¬∅.nontrivial
source
@[simp]
theorem set.not_nontrivial_singleton {α : Type u} {x : α} :
¬{x}.nontrivial
source
theorem set.nontrivial.ne_singleton {α : Type u} {s : set α} {x : α} (hs : s.nontrivial) :
s ≠ {x}
source
theorem set.nontrivial.not_subset_singleton {α : Type u} {s : set α} {x : α} (hs : s.nontrivial) :
¬s ⊆ {x}
source
theorem set.nontrivial_univ {α : Type u} [nontrivial α] :
set.univ.nontrivial
source
theorem set.nontrivial_of_univ_nontrivial {α : Type u} (h : set.univ.nontrivial) :
nontrivial α
source
@[simp]
theorem set.nontrivial_univ_iff {α : Type u} :
set.univ.nontrivial ↔ nontrivial α
source
theorem set.nontrivial_of_nontrivial {α : Type u} {s : set α} (hs : s.nontrivial) :
nontrivial α
source
@[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.

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

Alias of the reverse direction of set.nontrivial_coe_sort.

source
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.

source
theorem set.nontrivial_mono {α : Type u_1} {s t : set α} (hst : s ⊆ t) (hs : nontrivial ↥s) :
nontrivial ↥t
source
@[simp]
theorem set.not_subsingleton_iff {α : Type u} {s : set α} :
¬s.subsingleton ↔ s.nontrivial
source
@[simp]
theorem set.not_nontrivial_iff {α : Type u} {s : set α} :
¬s.nontrivial ↔ s.subsingleton
source
theorem set.subsingleton.not_nontrivial {α : Type u} {s : set α} :
s.subsingleton → ¬s.nontrivial

Alias of the reverse direction of set.not_nontrivial_iff.

source
theorem set.nontrivial.not_subsingleton {α : Type u} {s : set α} :
s.nontrivial → ¬s.subsingleton

Alias of the reverse direction of set.not_subsingleton_iff.

source
@[protected]
theorem set.subsingleton_or_nontrivial {α : Type u} (s : set α) :
s.subsingleton ∨ s.nontrivial
source
theorem set.eq_singleton_or_nontrivial {α : Type u} {a : α} {s : set α} (ha : a ∈ s) :
s = {a} ∨ s.nontrivial
source
theorem set.nontrivial_iff_ne_singleton {α : Type u} {a : α} {s : set α} (ha : a ∈ s) :
s.nontrivial ↔ s ≠ {a}
source
theorem set.nonempty.exists_eq_singleton_or_nontrivial {α : Type u} {s : set α} :
s.nonempty → (∃ (a : α), s = {a}) ∨ s.nontrivial
source
theorem set.univ_eq_true_false  :
set.univ = {true, false}
source
theorem set.monotone_on_iff_monotone {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] {f : α → β} :
monotone_on f s ↔ monotone (λ (a : ↥s), f ↑a)
source
theorem set.antitone_on_iff_antitone {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] {f : α → β} :
antitone_on f s ↔ antitone (λ (a : ↥s), f ↑a)
source
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)
source
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)

Monotonicity on singletons #

source
@[protected]
theorem set.subsingleton.monotone_on {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] (f : α → β) (h : s.subsingleton) :
monotone_on f s
source
@[protected]
theorem set.subsingleton.antitone_on {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] (f : α → β) (h : s.subsingleton) :
antitone_on f s
source
@[protected]
theorem set.subsingleton.strict_mono_on {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] (f : α → β) (h : s.subsingleton) :
strict_mono_on f s
source
@[protected]
theorem set.subsingleton.strict_anti_on {α : Type u} {β : Type v} {s : set α} [preorder α] [preorder β] (f : α → β) (h : s.subsingleton) :
strict_anti_on f s
source
@[simp]
theorem set.monotone_on_singleton {α : Type u} {β : Type v} {a : α} [preorder α] [preorder β] (f : α → β) :
monotone_on f {a}
source
@[simp]
theorem set.antitone_on_singleton {α : Type u} {β : Type v} {a : α} [preorder α] [preorder β] (f : α → β) :
antitone_on f {a}
source
@[simp]
theorem set.strict_mono_on_singleton {α : Type u} {β : Type v} {a : α} [preorder α] [preorder β] (f : α → β) :
strict_mono_on f {a}
source
@[simp]
theorem set.strict_anti_on_singleton {α : Type u} {β : Type v} {a : α} [preorder α] [preorder β] (f : α → β) :
strict_anti_on f {a}
source
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.

source
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.

source
theorem function.injective.nonempty_apply_iff {α : Type u_2} {β : Type u_3} {f : set α → set β} (hf : function.injective f) (h2 : f ∅ = ∅) {s : set α} :
(f s).nonempty ↔ s.nonempty

Lemmas about inclusion, the injection of subtypes induced by ⊆ #

source
def set.inclusion {α : Type u_1} {s t : set α} (h : s ⊆ t) :
↥s → ↥t

inclusion is the "identity" function between two subsets s and t, where s ⊆ t

Equations
source
@[simp]
theorem set.inclusion_self {α : Type u_1} {s : set α} (x : ↥s) :
set.inclusion set.subset.rfl x = x
source
theorem set.inclusion_eq_id {α : Type u_1} {s : set α} (h : s ⊆ s) :
set.inclusion h = id
source
@[simp]
theorem set.inclusion_mk {α : Type u_1} {s t : set α} {h : s ⊆ t} (a : α) (ha : a ∈ s) :
set.inclusion h ⟨a, ha⟩ = ⟨a, _⟩
source
theorem set.inclusion_right {α : Type u_1} {s t : set α} (h : s ⊆ t) (x : ↥t) (m : ↑x ∈ s) :
set.inclusion h ⟨↑x, m⟩ = x
source
@[simp]
theorem set.inclusion_inclusion {α : Type u_1} {s t u : set α} (hst : s ⊆ t) (htu : t ⊆ u) (x : ↥s) :
set.inclusion htu (set.inclusion hst x) = set.inclusion _ x
source
@[simp]
theorem set.inclusion_comp_inclusion {α : Type u_1} {s t u : set α} (hst : s ⊆ t) (htu : t ⊆ u) :
set.inclusion htu ∘ set.inclusion hst = set.inclusion _
source
@[simp]
theorem set.coe_inclusion {α : Type u_1} {s t : set α} (h : s ⊆ t) (x : ↥s) :
↑(set.inclusion h x) = ↑x
source
theorem set.inclusion_injective {α : Type u_1} {s t : set α} (h : s ⊆ t) :
function.injective (set.inclusion h)
source
theorem set.eq_of_inclusion_surjective {α : Type u_1} {s t : set α} {h : s ⊆ t} (h_surj : function.surjective (set.inclusion h)) :
s = t
source
theorem subsingleton.eq_univ_of_nonempty {α : Type u_1} [subsingleton α] {s : set α} :
s.nonempty → s = set.univ
source
theorem subsingleton.set_cases {α : Type u_1} [subsingleton α] {p : set α → Prop} (h0 : p ∅) (h1 : p set.univ) (s : set α) :
p s
source
theorem subsingleton.mem_iff_nonempty {α : Type u_1} [subsingleton α] {s : set α} {x : α} :
x ∈ s ↔ s.nonempty

Decidability instances for sets #

source
@[protected, instance]
def set.decidable_sdiff {α : Type u} (s t : set α) (a : α) [decidable (a ∈ s)] [decidable (a ∈ t)] :
decidable (a ∈ s \ t)
Equations
source
@[protected, instance]
def set.decidable_inter {α : Type u} (s t : set α) (a : α) [decidable (a ∈ s)] [decidable (a ∈ t)] :
decidable (a ∈ s ∩ t)
Equations
source
@[protected, instance]
def set.decidable_union {α : Type u} (s t : set α) (a : α) [decidable (a ∈ s)] [decidable (a ∈ t)] :
decidable (a ∈ s ∪ t)
Equations
source
@[protected, instance]
def set.decidable_compl {α : Type u} (s : set α) (a : α) [decidable (a ∈ s)] :
decidable (a ∈ sᶜ)
Equations
source
@[protected, instance]
def set.decidable_emptyset {α : Type u} :
decidable_pred (λ (_x : α), _x ∈ ∅)
Equations
source
@[protected, instance]
def set.decidable_univ {α : Type u} :
decidable_pred (λ (_x : α), _x ∈ set.univ)
Equations
source
@[protected, instance]
def set.decidable_set_of {α : Type u} (a : α) (p : α → Prop) [decidable (p a)] :
decidable (a ∈ {a : α | p a})
Equations

Monotone lemmas for sets #

source
theorem monotone.inter {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x ∩ g x)
source
theorem monotone_on.inter {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} {s : set β} (hf : monotone_on f s) (hg : monotone_on g s) :
monotone_on (λ (x : β), f x ∩ g x) s
source
theorem antitone.inter {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} (hf : antitone f) (hg : antitone g) :
antitone (λ (x : β), f x ∩ g x)
source
theorem antitone_on.inter {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} {s : set β} (hf : antitone_on f s) (hg : antitone_on g s) :
antitone_on (λ (x : β), f x ∩ g x) s
source
theorem monotone.union {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x ∪ g x)
source
theorem monotone_on.union {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} {s : set β} (hf : monotone_on f s) (hg : monotone_on g s) :
monotone_on (λ (x : β), f x ∪ g x) s
source
theorem antitone.union {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} (hf : antitone f) (hg : antitone g) :
antitone (λ (x : β), f x ∪ g x)
source
theorem antitone_on.union {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set α} {s : set β} (hf : antitone_on f s) (hg : antitone_on g s) :
antitone_on (λ (x : β), f x ∪ g x) s
source
theorem set.monotone_set_of {α : Type u_1} {β : Type u_2} [preorder α] {p : α → β → Prop} (hp : ∀ (b : β), monotone (λ (a : α), p a b)) :
monotone (λ (a : α), {b : β | p a b})
source
theorem set.antitone_set_of {α : Type u_1} {β : Type u_2} [preorder α] {p : α → β → Prop} (hp : ∀ (b : β), antitone (λ (a : α), p a b)) :
antitone (λ (a : α), {b : β | p a b})
source
theorem set.antitone_bforall {α : Type u_1} {P : α → Prop} :
antitone (λ (s : set α), ∀ (x : α), x ∈ s → P x)

Quantifying over a set is antitone in the set

Disjoint sets #

source
theorem disjoint.union_left {α : Type u_1} {s t u : set α} (hs : disjoint s u) (ht : disjoint t u) :
disjoint (s ∪ t) u
source
theorem disjoint.union_right {α : Type u_1} {s t u : set α} (ht : disjoint s t) (hu : disjoint s u) :
disjoint s (t ∪ u)
source
theorem disjoint.inter_left {α : Type u_1} {s t : set α} (u : set α) (h : disjoint s t) :
disjoint (s ∩ u) t
source
theorem disjoint.inter_left' {α : Type u_1} {s t : set α} (u : set α) (h : disjoint s t) :
disjoint (u ∩ s) t
source
theorem disjoint.inter_right {α : Type u_1} {s t : set α} (u : set α) (h : disjoint s t) :
disjoint s (t ∩ u)
source
theorem disjoint.inter_right' {α : Type u_1} {s t : set α} (u : set α) (h : disjoint s t) :
disjoint s (u ∩ t)
source
theorem disjoint.subset_left_of_subset_union {α : Type u_1} {s t u : set α} (h : s ⊆ t ∪ u) (hac : disjoint s u) :
s ⊆ t
source
theorem disjoint.subset_right_of_subset_union {α : Type u_1} {s t u : set α} (h : s ⊆ t ∪ u) (hab : disjoint s t) :
s ⊆ u
source
@[simp]
theorem Prop.compl_singleton (p : Prop) :
{p}ᶜ = {¬p}