data.set.basic

# Basic properties of sets #

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:

• `f : α → β` is a function,

• `s : set α` and `s₁ s₂ : set α` are subsets of `α`

• `t : set β` is a subset of `β`.

Definitions in the file:

• `nonempty s : Prop` : the predicate `s ≠ ∅`. Note that this is the preferred way to express the fact that `s` has an element (see the Implementation Notes).

• `preimage f t : set α` : the preimage f⁻¹(t) (written `f ⁻¹' t` in Lean) of a subset of β.

• `subsingleton s : Prop` : the predicate saying that `s` has at most one element.

• `nontrivial s : Prop` : the predicate saying that `s` has at least two distinct elements.

• `range f : set β` : the image of `univ` under `f`. Also works for `{p : Prop} (f : p → α)` (unlike `image`)

• `inclusion s₁ s₂ : ↥s₁ → ↥s₂` : the map `↥s₁ → ↥s₂` induced by an inclusion `s₁ ⊆ s₂`.

## Notation #

• `f ⁻¹' t` for `preimage f t`

• `f '' s` for `image f s`

• `sᶜ` for the complement of `s`

## Implementation notes #

• `s.nonempty` is to be preferred to `s ≠ ∅` or `∃ x, x ∈ s`. It has the advantage that the `s.nonempty` dot notation can be used.

• For `s : set α`, do not use `subtype s`. Instead use `↥s` or `(s : Type*)` or `s`.

## Tags #

set, sets, subset, subsets, image, preimage, pre-image, range, union, intersection, insert, singleton, complement, powerset

### Set coercion to a type #

@[protected, instance]
def set.has_le {α : Type u_1} :
has_le (set α)
Equations
@[protected, instance]
def set.has_subset {α : Type u_1} :
Equations
@[protected, instance]
def set.boolean_algebra {α : Type u_1} :
Equations
@[protected, instance]
def set.has_ssubset {α : Type u_1} :
Equations
@[protected, instance]
def set.has_union {α : Type u_1} :
Equations
@[protected, instance]
def set.has_inter {α : Type u_1} :
Equations
@[simp]
theorem set.top_eq_univ {α : Type u_1} :
@[simp]
theorem set.bot_eq_empty {α : Type u_1} :
@[simp]
theorem set.sup_eq_union {α : Type u_1} :
@[simp]
theorem set.inf_eq_inter {α : Type u_1} :
@[simp]
theorem set.le_eq_subset {α : Type u_1} :
@[simp]
theorem set.lt_eq_ssubset {α : Type u_1} :
@[protected, instance]
def set.has_coe_to_sort {α : Type u} :
(Type u)

Coercion from a set to the corresponding subtype.

Equations
@[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)
Equations
@[protected, instance]
def set.pi_set_coe.can_lift' (ι : Type u) (α : Type v) [ne : nonempty α] (s : set ι) :
can_lift (s → α) (ι → α)
Equations
• = (λ (_x : ι), α) s
theorem set.coe_eq_subtype {α : Type u} (s : set α) :
s = {x // x s}
@[simp]
theorem set.coe_set_of {α : Type u} (p : α → Prop) :
{x : α | p x} = {x // p x}
@[simp]
theorem set_coe.forall {α : Type u} {s : set α} {p : s → Prop} :
(∀ (x : s), p x) ∀ (x : α) (h : x s), p x, h⟩
@[simp]
theorem set_coe.exists {α : Type u} {s : set α} {p : s → Prop} :
(∃ (x : s), p x) ∃ (x : α) (h : x s), p x, h⟩
theorem set_coe.exists' {α : Type u} {s : set α} {p : Π (x : α), x s → Prop} :
(∃ (x : α) (h : x s), p x h) ∃ (x : s), p x _
theorem set_coe.forall' {α : Type u} {s : set α} {p : Π (x : α), x s → Prop} :
(∀ (x : α) (h : x s), p x h) ∀ (x : s), p x _
@[simp]
theorem set_coe_cast {α : Type u} {s t : set α} (H' : s = t) (H : s = t) (x : s) :
cast H x = x.val, _⟩
theorem set_coe.ext {α : Type u} {s : set α} {a b : s} :
a = ba = b
theorem set_coe.ext_iff {α : Type u} {s : set α} {a b : s} :
a = b a = b
theorem subtype.mem {α : Type u_1} {s : set α} (p : s) :
p s

See also `subtype.prop`

theorem eq.subset {α : Type u_1} {s t : set α} :
s = ts t

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

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

### Lemmas about `mem` and `set_of`#

theorem set.mem_set_of {α : Type u} {a : α} {p : α → Prop} :
a {x : α | p x} p a
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`.

theorem set.nmem_set_of_eq {α : Type u} {a : α} {p : α → Prop} :
a {x : α | p x} = ¬p a
@[simp]
theorem set.set_of_mem_eq {α : Type u} {s : set α} :
{x : α | x s} = s
theorem set.set_of_set {α : Type u} {s : set α} :
= s
theorem set.set_of_app_iff {α : Type u} {p : α → Prop} {x : α} :
{x : α | p x} x p x
theorem set.mem_def {α : Type u} {a : α} {s : set α} :
a s s a
theorem set.set_of_bijective {α : Type u} :
@[simp]
theorem set.set_of_subset_set_of {α : Type u} {p q : α → Prop} :
{a : α | p a} {a : α | q a} ∀ (a : α), p aq a
@[simp]
theorem set.sep_set_of {α : Type u} {p q : α → Prop} :
{a ∈ {a : α | p a} | q a} = {a : α | p a q a}
theorem set.set_of_and {α : Type u} {p q : α → Prop} :
{a : α | p a q a} = {a : α | p a} {a : α | q a}
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 #

@[protected, instance]
def set.has_subset.subset.is_refl {α : Type u} :
@[protected, instance]
def set.has_subset.subset.is_trans {α : Type u} :
@[protected, instance]
def set.has_subset.subset.is_antisymm {α : Type u} :
@[protected, instance]
def set.has_ssubset.ssubset.is_irrefl {α : Type u} :
@[protected, instance]
def set.has_ssubset.ssubset.is_trans {α : Type u} :
@[protected, instance]
def set.has_ssubset.ssubset.is_asymm {α : Type u} :
@[protected, instance]
Equations
theorem set.subset_def {α : Type u} {s t : set α} :
s t = ∀ (x : α), x sx t
theorem set.ssubset_def {α : Type u} {s t : set α} :
s t = (s t ¬t s)
@[refl]
theorem set.subset.refl {α : Type u} (a : set α) :
a a
theorem set.subset.rfl {α : Type u} {s : set α} :
s s
@[trans]
theorem set.subset.trans {α : Type u} {a b c : set α} (ab : a b) (bc : b c) :
a c
@[trans]
theorem set.mem_of_eq_of_mem {α : Type u} {x y : α} {s : set α} (hx : x = y) (h : y s) :
x s
theorem set.subset.antisymm {α : Type u} {a b : set α} (h₁ : a b) (h₂ : b a) :
a = b
theorem set.subset.antisymm_iff {α : Type u} {a b : set α} :
a = b a b b a
theorem set.eq_of_subset_of_subset {α : Type u} {a b : set α} :
a bb aa = b
theorem set.mem_of_subset_of_mem {α : Type u} {s₁ s₂ : set α} {a : α} (h : s₁ s₂) :
a s₁a s₂
theorem set.not_mem_subset {α : Type u} {a : α} {s t : set α} (h : s t) :
a ta s
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. #

@[protected]
theorem set.eq_or_ssubset_of_subset {α : Type u} {s t : set α} (h : s t) :
s = t s t
theorem set.exists_of_ssubset {α : Type u} {s t : set α} (h : s t) :
∃ (x : α) (H : x t), x s
@[protected]
theorem set.ssubset_iff_subset_ne {α : Type u} {s t : set α} :
s t s t s t
theorem set.ssubset_iff_of_subset {α : Type u} {s t : set α} (h : s t) :
s t ∃ (x : α) (H : x t), x s
@[protected]
theorem set.ssubset_of_ssubset_of_subset {α : Type u} {s₁ s₂ s₃ : set α} (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
s₁ s₃
@[protected]
theorem set.ssubset_of_subset_of_ssubset {α : Type u} {s₁ s₂ s₃ : set α} (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
s₁ s₃
theorem set.not_mem_empty {α : Type u} (x : α) :
@[simp]
theorem set.not_not_mem {α : Type u} {a : α} {s : set α} :
¬a s a s

### Non-empty sets #

@[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
@[simp]
theorem set.nonempty_coe_sort {α : Type u} {s : set α} :
theorem set.nonempty_def {α : Type u} {s : set α} :
s.nonempty ∃ (x : α), x s
theorem set.nonempty_of_mem {α : Type u} {s : set α} {x : α} (h : x s) :
theorem set.nonempty.not_subset_empty {α : Type u} {s : set α} :
theorem set.nonempty.ne_empty {α : Type u} {s : set α} :
s.nonemptys
@[simp]
theorem set.not_nonempty_empty {α : Type u} :
@[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
@[protected]
theorem set.nonempty.some_mem {α : Type u} {s : set α} (h : s.nonempty) :
h.some s
theorem set.nonempty.mono {α : Type u} {s t : set α} (ht : s t) (hs : s.nonempty) :
theorem set.nonempty_of_not_subset {α : Type u} {s t : set α} (h : ¬s t) :
(s \ t).nonempty
theorem set.nonempty_of_ssubset {α : Type u} {s t : set α} (ht : s t) :
(t \ s).nonempty
theorem set.nonempty.of_diff {α : Type u} {s t : set α} (h : (s \ t).nonempty) :
theorem set.nonempty_of_ssubset' {α : Type u} {s t : set α} (ht : s t) :
theorem set.nonempty.inl {α : Type u} {s t : set α} (hs : s.nonempty) :
theorem set.nonempty.inr {α : Type u} {s t : set α} (ht : t.nonempty) :
@[simp]
theorem set.union_nonempty {α : Type u} {s t : set α} :
theorem set.nonempty.left {α : Type u} {s t : set α} (h : (s t).nonempty) :
theorem set.nonempty.right {α : Type u} {s t : set α} (h : (s t).nonempty) :
theorem set.inter_nonempty {α : Type u} {s t : set α} :
(s t).nonempty ∃ (x : α), x s x t
theorem set.inter_nonempty_iff_exists_left {α : Type u} {s t : set α} :
(s t).nonempty ∃ (x : α) (H : x s), x t
theorem set.inter_nonempty_iff_exists_right {α : Type u} {s t : set α} :
(s t).nonempty ∃ (x : α) (H : x t), x s
theorem set.nonempty_iff_univ_nonempty {α : Type u} :
@[simp]
theorem set.univ_nonempty {α : Type u} [h : nonempty α] :
theorem set.nonempty.to_subtype {α : Type u} {s : set α} (h : s.nonempty) :
@[protected, instance]
def set.univ.nonempty {α : Type u} [nonempty α] :
theorem set.nonempty_of_nonempty_subtype {α : Type u} {s : set α} [nonempty s] :

### Lemmas about the empty set #

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

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

Equations
theorem set.not_nonempty_iff_eq_empty {α : Type u} {s : set α} :
theorem set.empty_not_nonempty {α : Type u} :
theorem set.ne_empty_iff_nonempty {α : Type u} {s : set α} :
@[simp]
theorem set.is_empty_coe_sort {α : Type u} {s : set α} :
s =
theorem set.eq_empty_or_nonempty {α : Type u} (s : set α) :
theorem set.subset_eq_empty {α : Type u} {s t : set α} (h : t s) (e : s = ) :
t =
theorem set.ball_empty_iff {α : Type u} {p : α → Prop} :
(∀ (x : α), x p x) true
@[protected, instance]
def set.has_emptyc.emptyc.is_empty (α : Type u) :
@[simp]
theorem set.empty_ssubset {α : Type u} {s : set α} :

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

@[simp]
theorem set.set_of_true {α : Type u} :
{x : α | true} = set.univ
@[simp]
theorem set.mem_univ {α : Type u} (x : α) :
@[simp]
theorem set.univ_eq_empty_iff {α : Type u} :
theorem set.empty_ne_univ {α : Type u} [nonempty α] :
@[simp]
theorem set.subset_univ {α : Type u} (s : set α) :
theorem set.univ_subset_iff {α : Type u} {s : set α} :
theorem set.eq_univ_of_univ_subset {α : Type u} {s : set α} :
theorem set.eq_univ_iff_forall {α : Type u} {s : set α} :
∀ (x : α), x s
theorem set.eq_univ_of_forall {α : Type u} {s : set α} :
(∀ (x : α), x s)
theorem set.eq_univ_of_subset {α : Type u} {s t : set α} (h : s t) (hs : s = set.univ) :
theorem set.exists_mem_of_nonempty (α : Type u_1) [nonempty α] :
∃ (x : α),
theorem set.ne_univ_iff_exists_not_mem {α : Type u_1} (s : set α) :
∃ (a : α), a s
theorem set.not_subset_iff_exists_mem_not_mem {α : Type u_1} {s t : set α} :
¬s t ∃ (x : α), x s x t
theorem set.univ_unique {α : Type u} [unique α] :
@[protected, instance]
def set.nontrivial_of_nonempty {α : Type u} [nonempty α] :

theorem set.union_def {α : Type u} {s₁ s₂ : set α} :
s₁ s₂ = {a : α | a s₁ a s₂}
theorem set.mem_union_left {α : Type u} {x : α} {a : set α} (b : set α) :
x ax a b
theorem set.mem_union_right {α : Type u} {x : α} {b : set α} (a : set α) :
x bx a b
theorem set.mem_or_mem_of_mem_union {α : Type u} {x : α} {a b : set α} (H : x a b) :
x a x b
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
theorem set.mem_union {α : Type u} (x : α) (a b : set α) :
x a b x a x b
@[simp]
theorem set.mem_union_eq {α : Type u} (x : α) (a b : set α) :
x a b = (x a x b)
@[simp]
theorem set.union_self {α : Type u} (a : set α) :
a a = a
@[simp]
theorem set.union_empty {α : Type u} (a : set α) :
a = a
@[simp]
theorem set.empty_union {α : Type u} (a : set α) :
a = a
theorem set.union_comm {α : Type u} (a b : set α) :
a b = b a
theorem set.union_assoc {α : Type u} (a b c : set α) :
a b c = a (b c)
@[protected, instance]
def set.union_is_assoc {α : Type u} :
@[protected, instance]
def set.union_is_comm {α : Type u} :
theorem set.union_left_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ (s₂ s₃) = s₂ (s₁ s₃)
theorem set.union_right_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ s₂ s₃ = s₁ s₃ s₂
@[simp]
theorem set.union_eq_left_iff_subset {α : Type u} {s t : set α} :
s t = s t s
@[simp]
theorem set.union_eq_right_iff_subset {α : Type u} {s t : set α} :
s t = t s t
theorem set.union_eq_self_of_subset_left {α : Type u} {s t : set α} (h : s t) :
s t = t
theorem set.union_eq_self_of_subset_right {α : Type u} {s t : set α} (h : t s) :
s t = s
@[simp]
theorem set.subset_union_left {α : Type u} (s t : set α) :
s s t
@[simp]
theorem set.subset_union_right {α : Type u} (s t : set α) :
t s t
theorem set.union_subset {α : Type u} {s t r : set α} (sr : s r) (tr : t r) :
s t r
@[simp]
theorem set.union_subset_iff {α : Type u} {s t u : set α} :
s t u s u t u
theorem set.union_subset_union {α : Type u} {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ s₂) (h₂ : t₁ t₂) :
s₁ t₁ s₂ t₂
theorem set.union_subset_union_left {α : Type u} {s₁ s₂ : set α} (t : set α) (h : s₁ s₂) :
s₁ t s₂ t
theorem set.union_subset_union_right {α : Type u} (s : set α) {t₁ t₂ : set α} (h : t₁ t₂) :
s t₁ s t₂
theorem set.subset_union_of_subset_left {α : Type u} {s t : set α} (h : s t) (u : set α) :
s t u
theorem set.subset_union_of_subset_right {α : Type u} {s u : set α} (h : s u) (t : set α) :
s t u
theorem set.union_congr_left {α : Type u} {s t u : set α} (ht : t s u) (hu : u s t) :
s t = s u
theorem set.union_congr_right {α : Type u} {s t u : set α} (hs : s t u) (ht : t s u) :
s u = t u
theorem set.union_eq_union_iff_left {α : Type u} {s t u : set α} :
s t = s u t s u u s t
theorem set.union_eq_union_iff_right {α : Type u} {s t u : set α} :
s u = t u s t u t s u
@[simp]
theorem set.union_empty_iff {α : Type u} {s t : set α} :
s t = s = t =
@[simp]
theorem set.union_univ {α : Type u} {s : set α} :
@[simp]
theorem set.univ_union {α : Type u} {s : set α} :

theorem set.inter_def {α : Type u} {s₁ s₂ : set α} :
s₁ s₂ = {a : α | a s₁ a s₂}
theorem set.mem_inter_iff {α : Type u} (x : α) (a b : set α) :
x a b x a x b
@[simp]
theorem set.mem_inter_eq {α : Type u} (x : α) (a b : set α) :
x a b = (x a x b)
theorem set.mem_inter {α : Type u} {x : α} {a b : set α} (ha : x a) (hb : x b) :
x a b
theorem set.mem_of_mem_inter_left {α : Type u} {x : α} {a b : set α} (h : x a b) :
x a
theorem set.mem_of_mem_inter_right {α : Type u} {x : α} {a b : set α} (h : x a b) :
x b
@[simp]
theorem set.inter_self {α : Type u} (a : set α) :
a a = a
@[simp]
theorem set.inter_empty {α : Type u} (a : set α) :
@[simp]
theorem set.empty_inter {α : Type u} (a : set α) :
theorem set.inter_comm {α : Type u} (a b : set α) :
a b = b a
theorem set.inter_assoc {α : Type u} (a b c : set α) :
a b c = a (b c)
@[protected, instance]
def set.inter_is_assoc {α : Type u} :
@[protected, instance]
def set.inter_is_comm {α : Type u} :
theorem set.inter_left_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ (s₂ s₃) = s₂ (s₁ s₃)
theorem set.inter_right_comm {α : Type u} (s₁ s₂ s₃ : set α) :
s₁ s₂ s₃ = s₁ s₃ s₂
@[simp]
theorem set.inter_subset_left {α : Type u} (s t : set α) :
s t s
@[simp]
theorem set.inter_subset_right {α : Type u} (s t : set α) :
s t t
theorem set.subset_inter {α : Type u} {s t r : set α} (rs : r s) (rt : r t) :
r s t
@[simp]
theorem set.subset_inter_iff {α : Type u} {s t r : set α} :
r s t r s r t
@[simp]
theorem set.inter_eq_left_iff_subset {α : Type u} {s t : set α} :
s t = s s t
@[simp]
theorem set.inter_eq_right_iff_subset {α : Type u} {s t : set α} :
s t = t t s
theorem set.inter_eq_self_of_subset_left {α : Type u} {s t : set α} :
s ts t = s
theorem set.inter_eq_self_of_subset_right {α : Type u} {s t : set α} :
t ss t = t
theorem set.inter_congr_left {α : Type u} {s t u : set α} (ht : s u t) (hu : s t u) :
s t = s u
theorem set.inter_congr_right {α : Type u} {s t u : set α} (hs : t u s) (ht : s u t) :
s u = t u
theorem set.inter_eq_inter_iff_left {α : Type u} {s t u : set α} :
s t = s u s u t s t u
theorem set.inter_eq_inter_iff_right {α : Type u} {s t u : set α} :
s u = t u t u s s u t
@[simp]
theorem set.inter_univ {α : Type u} (a : set α) :
= a
@[simp]
theorem set.univ_inter {α : Type u} (a : set α) :
= a
theorem set.inter_subset_inter {α : Type u} {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ t₁) (h₂ : s₂ t₂) :
s₁ s₂ t₁ t₂
theorem set.inter_subset_inter_left {α : Type u} {s t : set α} (u : set α) (H : s t) :
s u t u
theorem set.inter_subset_inter_right {α : Type u} {s t : set α} (u : set α) (H : s t) :
u s u t
theorem set.union_inter_cancel_left {α : Type u} {s t : set α} :
(s t) s = s
theorem set.union_inter_cancel_right {α : Type u} {s t : set α} :
(s t) t = t

### Distributivity laws #

theorem set.inter_distrib_left {α : Type u} (s t u : set α) :
s (t u) = s t s u
theorem set.inter_union_distrib_left {α : Type u} {s t u : set α} :
s (t u) = s t s u
theorem set.inter_distrib_right {α : Type u} (s t u : set α) :
(s t) u = s u t u
theorem set.union_inter_distrib_right {α : Type u} {s t u : set α} :
(s t) u = s u t u
theorem set.union_distrib_left {α : Type u} (s t u : set α) :
s t u = (s t) (s u)
theorem set.union_inter_distrib_left {α : Type u} {s t u : set α} :
s t u = (s t) (s u)
theorem set.union_distrib_right {α : Type u} (s t u : set α) :
s t u = (s u) (t u)
theorem set.inter_union_distrib_right {α : Type u} {s t u : set α} :
s t u = (s u) (t u)
theorem set.union_union_distrib_left {α : Type u} (s t u : set α) :
s (t u) = s t (s u)
theorem set.union_union_distrib_right {α : Type u} (s t u : set α) :
s t u = s u (t u)
theorem set.inter_inter_distrib_left {α : Type u} (s t u : set α) :
s (t u) = s t (s u)
theorem set.inter_inter_distrib_right {α : Type u} (s t u : set α) :
s t u = s u (t u)
theorem set.union_union_union_comm {α : Type u} (s t u v : set α) :
s t (u v) = s u (t v)
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`.

theorem set.insert_def {α : Type u} (x : α) (s : set α) :
= {y : α | y = x y s}
@[simp]
theorem set.subset_insert {α : Type u} (x : α) (s : set α) :
s
theorem set.mem_insert {α : Type u} (x : α) (s : set α) :
x
theorem set.mem_insert_of_mem {α : Type u} {x : α} {s : set α} (y : α) :
x sx
theorem set.eq_or_mem_of_mem_insert {α : Type u} {x a : α} {s : set α} :
x x = a x s
theorem set.mem_of_mem_insert_of_ne {α : Type u} {a b : α} {s : set α} :
b b ab s
theorem set.eq_of_not_mem_of_mem_insert {α : Type u} {a b : α} {s : set α} :
b b sb = a
@[simp]
theorem set.mem_insert_iff {α : Type u} {x a : α} {s : set α} :
x x = a x s
@[simp]
theorem set.insert_eq_of_mem {α : Type u} {a : α} {s : set α} (h : a s) :
= s
theorem set.ne_insert_of_not_mem {α : Type u} {s : set α} (t : set α) {a : α} :
a ss
@[simp]
theorem set.insert_eq_self {α : Type u} {a : α} {s : set α} :
= s a s
theorem set.insert_ne_self {α : Type u} {a : α} {s : set α} :
s a s
theorem set.insert_subset {α : Type u} {a : α} {s t : set α} :
t a t s t
theorem set.insert_subset_insert {α : Type u} {a : α} {s t : set α} (h : s t) :
theorem set.insert_subset_insert_iff {α : Type u} {a : α} {s t : set α} (ha : a s) :
s t
theorem set.ssubset_iff_insert {α : Type u} {s t : set α} :
s t ∃ (a : α) (H : a s), t
theorem set.ssubset_insert {α : Type u} {s : set α} {a : α} (h : a s) :
s
theorem set.insert_comm {α : Type u} (a b : α) (s : set α) :
=
@[simp]
theorem set.insert_idem {α : Type u} (a : α) (s : set α) :
=
theorem set.insert_union {α : Type u} {a : α} {s t : set α} :
t = (s t)
@[simp]
theorem set.union_insert {α : Type u} {a : α} {s t : set α} :
s = (s t)
@[simp]
theorem set.insert_nonempty {α : Type u} (a : α) (s : set α) :
@[protected, instance]
def set.has_insert.insert.nonempty {α : Type u} (a : α) (s : set α) :
theorem set.insert_inter_distrib {α : Type u} (a : α) (s t : set α) :
(s t) =
theorem set.insert_union_distrib {α : Type u} (a : α) (s t : set α) :
(s t) =
theorem set.insert_inj {α : Type u} {a b : α} {s : set α} (ha : a s) :
a = b
theorem set.forall_of_forall_insert {α : Type u} {P : α → Prop} {a : α} {s : set α} (H : ∀ (x : α), x P x) (x : α) (h : x s) :
P x
theorem set.forall_insert_of_forall {α : Type u} {P : α → Prop} {a : α} {s : set α} (H : ∀ (x : α), x sP x) (ha : P a) (x : α) (h : x ) :
P x
theorem set.bex_insert_iff {α : Type u} {P : α → Prop} {a : α} {s : set α} :
(∃ (x : α) (H : x , P x) P a ∃ (x : α) (H : x s), P x
theorem set.ball_insert_iff {α : Type u} {P : α → Prop} {a : α} {s : set α} :
(∀ (x : α), x P x) P a ∀ (x : α), x sP 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
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 α) :
= {x} s
@[simp]
theorem set.pair_eq_singleton {α : Type u} (a : α) :
{a, a} = {a}
theorem set.pair_comm {α : Type u} (a b : α) :
{a, b} = {b, a}
@[simp]
theorem set.singleton_nonempty {α : Type u} (a : α) :
@[simp]
theorem set.singleton_subset_iff {α : Type u} {a : α} {s : set α} :
{a} s a s
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 =
@[simp]
theorem set.union_singleton {α : Type u} {a : α} {s : set α} :
s {a} =
@[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 α} :
@[protected, instance]
def set.unique_singleton {α : Type u} (a : α) :
Equations
theorem set.eq_singleton_iff_unique_mem {α : Type u} {a : α} {s : set α} :
s = {a} a s ∀ (x : α), x sx = a
theorem set.eq_singleton_iff_nonempty_unique_mem {α : Type u} {a : α} {s : set α} :
s = {a} s.nonempty ∀ (x : α), x sx = a
@[simp]
theorem set.default_coe_singleton {α : Type u} (x : α) :

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

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_eq {α : Type u} {s : set α} {p : α → Prop} {x : α} :
x {x ∈ s | p x} = (x s p x)
theorem set.mem_sep_iff {α : Type u} {s : set α} {p : α → Prop} {x : α} :
x {x ∈ s | p x} x s p x
theorem set.eq_sep_of_subset {α : Type u} {s t : set α} (h : s t) :
s = {x ∈ t | x s}
@[simp]
theorem set.sep_subset {α : Type u} (s : set α) (p : α → Prop) :
{x ∈ s | p x} s
@[simp]
theorem set.sep_empty {α : Type u} (p : α → Prop) :
{x ∈ | p x} =
theorem set.forall_not_of_sep_empty {α : Type u} {s : set α} {p : α → Prop} (H : {x ∈ s | p x} = ) (x : α) :
x s¬p x
@[simp]
theorem set.sep_univ {α : Type u_1} {p : α → Prop} :
{a ∈ set.univ | p a} = {a : α | p a}
@[simp]
theorem set.sep_true {α : Type u} {s : set α} :
{a ∈ s | true} = s
@[simp]
theorem set.sep_false {α : Type u} {s : set α} :
{a ∈ s | false} =
theorem set.sep_inter_sep {α : Type u} {s : set α} {p q : α → Prop} :
{x ∈ s | p x} {x ∈ s | q x} = {x ∈ s | p x q x}
@[simp]
theorem set.subset_singleton_iff {α : Type u_1} {s : set α} {x : α} :
s {x} ∀ (y : α), y sy = 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 =

### Disjointness #

theorem disjoint.inter_eq {α : Type u} {s t : set α} :
ts t =
theorem set.disjoint_left {α : Type u} {s t : set α} :
t ∀ ⦃a : α⦄, a sa t
theorem set.disjoint_right {α : Type u} {s t : set α} :
t ∀ ⦃a : α⦄, a ta s

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_eq {α : Type u} (s : set α) (x : α) :
x s = (x s)
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 α) :
@[simp]
theorem set.compl_inter_self {α : Type u} (s : set α) :
@[simp]
theorem set.compl_empty {α : Type u} :
@[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} :
@[simp]
theorem set.compl_empty_iff {α : Type u} {s : set α} :
@[simp]
theorem set.compl_univ_iff {α : Type u} {s : set α} :
s =
theorem set.compl_ne_univ {α : Type u} {s : set α} :
theorem set.nonempty_compl {α : Type u} {s : set α} :
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 α) :
@[simp]
theorem set.compl_union_self {α : Type u} (s : set α) :
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 s
theorem set.subset_compl_iff_disjoint_right {α : Type u} {s t : set α} :
s t t
theorem set.disjoint_compl_left_iff_subset {α : Type u} {s t : set α} :
t t s
theorem set.disjoint_compl_right_iff_subset {α : Type u} {s t : set α} :
t s t
theorem disjoint.subset_compl_right {α : Type u} {s t : set α} :
ts t

Alias of the reverse direction of `set.subset_compl_iff_disjoint_right`.

theorem disjoint.subset_compl_left {α : Type u} {s t : set α} :
ss 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 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 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 α} :
@[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 α} :

### Lemmas about set difference #

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.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 =
@[simp]
theorem set.empty_diff {α : Type u} (s : set α) :
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 α) :
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
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 (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) :
\ t = s \ t
theorem set.insert_diff_of_not_mem {α : Type u} {a : α} {t : set α} (s : set α) (h : a t) :
\ t = (s \ t)
theorem set.insert_diff_self_of_not_mem {α : Type u} {a : α} {s : set α} (h : a s) :
\ {a} = s
@[simp]
theorem set.insert_diff_eq_singleton {α : Type u} {a : α} {s : set α} (h : a s) :
\ s = {a}
theorem set.inter_insert_of_mem {α : Type u} {a : α} {s t : set α} (h : a s) :
s = (s t)
theorem set.insert_inter_of_mem {α : Type u} {a : α} {s t : set α} (h : a t) :
t = (s t)
theorem set.inter_insert_of_not_mem {α : Type u} {a : α} {s t : set α} (h : a s) :
s = s t
theorem set.insert_inter_of_not_mem {α : Type u} {a : α} {s t : set α} (h : a t) :
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_eq_self {α : Type u} {s t : set α} :
s \ t = s t s
@[simp]
theorem set.diff_singleton_eq_self {α : Type u} {a : α} {s : set α} (h : a s) :
s \ {a} = s
@[simp]
theorem set.insert_diff_singleton {α : Type u} {a : α} {s : set α} :
(s \ {a}) =
@[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

### Powerset #

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

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

Equations
theorem set.mem_powerset {α : Type u} {x s : set α} (h : 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 α) :
@[simp]
theorem set.powerset_mono {α : Type u} {s t : set α} :
theorem set.monotone_powerset {α : Type u} :
@[simp]
theorem set.powerset_nonempty {α : Type u} {s : set α} :
@[simp]
theorem set.powerset_empty {α : Type u} :
@[simp]
theorem set.powerset_univ {α : Type u} :

### If-then-else for sets #

@[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
@[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 α) :
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'

### Inverse image #

def set.preimage {α : Type u} {β : Type v} (f : α → β) (s : set β) :
set α

The preimage of `s : set β` by `f : α → β`, written `f ⁻¹' s`, is the set of `x : α` such that `f x ∈ s`.

Equations
Instances for `↥set.preimage`
@[simp]
theorem set.preimage_empty {α : Type u} {β : Type v} {f : α → β} :
@[simp]
theorem set.mem_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} {a : α} :
a f ⁻¹' s f a s
theorem set.preimage_congr {α : Type u} {β : Type v} {f g : α → β} {s : set β} (h : ∀ (x : α), f x = g x) :
f ⁻¹' s = g ⁻¹' s
theorem set.preimage_mono {α : Type u} {β : Type v} {f : α → β} {s t : set β} (h : s t) :
f ⁻¹' s f ⁻¹' t
@[simp]
theorem set.preimage_univ {α : Type u} {β : Type v} {f : α → β} :
theorem set.subset_preimage_univ {α : Type u} {β : Type v} {f : α → β} {s : set α} :
s
@[simp]
theorem set.preimage_inter {α : Type u} {β : Type v} {f : α → β} {s t : set β} :
f ⁻¹' (s t) = f ⁻¹' s f ⁻¹' t
@[simp]
theorem set.preimage_union {α : Type u} {β : Type v} {f : α → β} {s t : set β} :
f ⁻¹' (s t) = f ⁻¹' s f ⁻¹' t
@[simp]
theorem set.preimage_compl {α : Type u} {β : Type v} {f : α → β} {s : set β} :
@[simp]
theorem set.preimage_diff {α : Type u} {β : Type v} (f : α → β) (s t : set β) :
f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t
@[simp]
theorem set.preimage_ite {α : Type u} {β : Type v} (f : α → β) (s t₁ t₂ : set β) :
f ⁻¹' s.ite t₁ t₂ = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂)
@[simp]
theorem set.preimage_set_of_eq {α : Type u} {β : Type v} {p : α → Prop} {f : β → α} :
f ⁻¹' {a : α | p a} = {a : β | p (f a)}
@[simp]
theorem set.preimage_id {α : Type u} {s : set α} :
= s
@[simp]
theorem set.preimage_id' {α : Type u} {s : set α} :
(λ (x : α), x) ⁻¹' s = s
@[simp]
theorem set.preimage_const_of_mem {α : Type u} {β : Type v} {b : β} {s : set β} (h : b s) :
(λ (x : α), b) ⁻¹' s = set.univ
@[simp]
theorem set.preimage_const_of_not_mem {α : Type u} {β : Type v} {b : β} {s : set β} (h : b s) :
(λ (x : α), b) ⁻¹' s =
theorem set.preimage_const {α : Type u} {β : Type v} (b : β) (s : set β) [decidable (b s)] :
(λ (x : α), b) ⁻¹' s = ite (b s) set.univ
theorem set.preimage_comp {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {s : set γ} :
g f ⁻¹' s = f ⁻¹' (g ⁻¹' s)
theorem set.preimage_preimage {α : Type u} {β : Type v} {γ : Type w} {g : β → γ} {f : α → β} {s : set γ} :
f ⁻¹' (g ⁻¹' s) = (λ (x : α), g (f x)) ⁻¹' s
theorem set.eq_preimage_subtype_val_iff {α : Type u} {p : α → Prop} {s : set (subtype p)} {t : set α} :
s = ∀ (x : α) (h : p x), x, h⟩ s x t
theorem set.nonempty_of_nonempty_preimage {α : Type u} {β : Type v} {s : set β} {f : α → β} (hf : (f ⁻¹' s).nonempty) :

### Image of a set under a function #

def set.image {α : Type u} {β : Type v} (f : α → β) (s : set α) :
set β

The image of `s : set α` by `f : α → β`, written `f '' s`, is the set of `y : β` such that `f x = y` for some `x ∈ s`.

Equations
• f '' s = {y : β | ∃ (x : α), x s f x = y}
Instances for `set.image`
Instances for `↥set.image`
theorem set.mem_image_iff_bex {α : Type u} {β : Type v} {f : α → β} {s : set α} {y : β} :
y f '' s ∃ (x : α) (_x : x s), f x = y
theorem set.mem_image_eq {α : Type u} {β : Type v} (f : α → β) (s : set α) (y : β) :
y f '' s = ∃ (x : α), x s f x = y
@[simp]
theorem set.mem_image {α : Type u} {β : Type v} (f : α → β) (s : set α) (y : β) :
y f '' s ∃ (x : α), x s f x = y
theorem set.image_eta {α : Type u} {β : Type v} {s : set α} (f : α → β) :
f '' s = (λ (x : α), f x) '' s
theorem set.mem_image_of_mem {α : Type u} {β : Type v} (f : α → β) {x : α} {a : set α} (h : x a) :
f x f '' a
theorem function.injective.mem_set_image {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) {s : set α} {a : α} :
f a f '' s a s
theorem set.ball_image_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} {p : β → Prop} :
(∀ (y : β), y f '' sp y) ∀ (x : α), x sp (f x)
theorem set.ball_image_of_ball {α : Type u} {β : Type v} {f : α → β} {s : set α} {p : β → Prop} (h : ∀ (x : α), x sp (f x)) (y : β) (H : y f '' s) :
p y
theorem set.bex_image_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} {p : β → Prop} :
(∃ (y : β) (H : y f '' s), p y) ∃ (x : α) (H : x s), p (f x)
theorem set.mem_image_elim {α : Type u} {β : Type v} {f : α → β} {s : set α} {C : β → Prop} (h : ∀ (x : α), x sC (f x)) {y : β} :
y f '' sC y
theorem set.mem_image_elim_on {α : Type u} {β : Type v} {f : α → β} {s : set α} {C : β → Prop} {y : β} (h_y : y f '' s) (h : ∀ (x : α), x sC (f x)) :
C y
theorem set.image_congr {α : Type u} {β : Type v} {f g : α → β} {s : set α} (h : ∀ (a : α), a sf a = g a) :
f '' s = g '' s
theorem set.image_congr' {α : Type u} {β : Type v} {f g : α → β} {s : set α} (h : ∀ (x : α), f x = g x) :
f '' s = g '' s

A common special case of `image_congr`

theorem set.image_comp {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) (g : α → β) (a : set α) :
f g '' a = f '' (g '' a)
theorem set.image_image {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (s : set α) :
g '' (f '' s) = (λ (x : α), g (f x)) '' s

A variant of `image_comp`, useful for rewriting

theorem set.image_comm {α : Type u} {β : Type v} {γ : Type w} {s : set α} {β' : Type u_1} {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ} (h_comm : ∀ (a : α), f (g a) = g' (f' a)) :
f '' (g '' s) = g' '' (f' '' s)
theorem function.semiconj.set_image {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β} (h : gb) :
(set.image ga) (set.image gb)
theorem function.commute.set_image {α : Type u} {f g : α → α} (h : g) :
theorem set.image_subset {α : Type u} {β : Type v} {a b : set α} (f : α → β) (h : a b) :
f '' a f '' b

Image is monotone with respect to `⊆`. See `set.monotone_image` for the statement in terms of `≤`.

theorem set.image_union {α : Type u} {β : Type v} (f : α → β) (s t : set α) :
f '' (s t) = f '' s f '' t
@[simp]
theorem set.image_empty {α : Type u} {β : Type v} (f : α → β) :
theorem set.image_inter_subset {α : Type u} {β : Type v} (f : α → β) (s t : set α) :
f '' (s t) f '' s f '' t
theorem set.image_inter_on {α : Type u} {β : Type v} {f : α → β} {s t : set α} (h : ∀ (x : α), x t∀ (y : α), y sf x = f yx = y) :
f '' s f '' t = f '' (s t)
theorem set.image_inter {α : Type u} {β : Type v} {f : α → β} {s t : set α} (H : function.injective f) :
f '' s f '' t = f '' (s t)
theorem set.image_univ_of_surjective {β : Type v} {ι : Type u_1} {f : ι → β} (H : function.surjective f) :
@[simp]
theorem set.image_singleton {α : Type u} {β : Type v} {f : α → β} {a : α} :
f '' {a} = {f a}
@[simp]
theorem set.nonempty.image_const {α : Type u} {β : Type v} {s : set α} (hs : s.nonempty) (a : β) :
(λ (_x : α), a) '' s = {a}
@[simp]
theorem set.image_eq_empty {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :
f '' s = s =
theorem set.preimage_compl_eq_image_compl {α : Type u} (S : set α) :
theorem set.mem_compl_image {α : Type u} (t : α) (S : set α) :
t S
@[simp]
theorem set.image_id' {α : Type u} (s : set α) :
(λ (x : α), x) '' s = s

A variant of `image_id`

theorem set.image_id {α : Type u} (s : set α) :
id '' s = s
theorem set.compl_compl_image {α : Type u} (S : set α) :
theorem set.image_insert_eq {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} :
f '' = has_insert.insert (f a) (f '' s)
theorem set.image_pair {α : Type u} {β : Type v} (f : α → β) (a b : α) :
f '' {a, b} = {f a, f b}
theorem set.image_subset_preimage_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} (I : f) (s : set α) :
f '' s g ⁻¹' s
theorem set.preimage_subset_image_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} (I : f) (s : set β) :
f ⁻¹' s g '' s
theorem set.image_eq_preimage_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h₁ : f) (h₂ : f) :
theorem set.mem_image_iff_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} {b : β} {s : set α} (h₁ : f) (h₂ : f) :
b f '' s g b s
theorem set.image_compl_subset {α : Type u} {β : Type v} {f : α → β} {s : set α} (H : function.injective f) :
f '' s (f '' s)
theorem set.subset_image_compl {α : Type u} {β : Type v} {f : α → β} {s : set α} (H : function.surjective f) :
(f '' s) f '' s
theorem set.image_compl_eq {α : Type u} {β : Type v} {f : α → β} {s : set α} (H : function.bijective f) :
f '' s = (f '' s)
theorem set.subset_image_diff {α : Type u} {β : Type v} (f : α → β) (s t : set α) :
f '' s \ f '' t f '' (s \ t)
theorem set.image_diff {α : Type u} {β : Type v} {f : α → β} (hf : function.injective f) (s t : set α) :
f '' (s \ t) = f '' s \ f '' t
theorem set.nonempty.image {α : Type u} {β : Type v} (f : α → β) {s : set α} :
s.nonempty(f '' s).nonempty
theorem set.nonempty.of_image {α : Type u} {β : Type v} {f : α → β} {s : set α} :
(f '' s).nonempty → s.nonempty
@[simp]
theorem set.nonempty_image_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} :
theorem set.nonempty.preimage {α : Type u} {β : Type v} {s : set β} (hs : s.nonempty) {f : α → β} (hf : function.surjective f) :
@[protected, instance]
def set.image.nonempty {α : Type u} {β : Type v} (f : α → β) (s : set α) [nonempty s] :
@[simp]
theorem set.image_subset_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {f : α → β} :
f '' s t s f ⁻¹' t

image and preimage are a Galois connection

theorem set.image_preimage_subset {α : Type u} {β : Type v} (f : α → β) (s : set β) :
f '' (f ⁻¹' s) s
theorem set.subset_preimage_image {α : Type u} {β : Type v} (f : α → β) (s : set α) :
s f ⁻¹' (f '' s)
theorem set.preimage_image_eq {α : Type u} {β : Type v} {f : α → β} (s : set α) (h : function.injective f) :
f ⁻¹' (f '' s) = s
theorem set.image_preimage_eq {α : Type u} {β : Type v} {f : α → β} (s : set β) (h : function.surjective f) :
f '' (f ⁻¹' s) = s
theorem set.preimage_eq_preimage {α : Type u} {β : Type v} {s t : set α} {f : β → α} (hf : function.surjective f) :
f ⁻¹' s = f ⁻¹' t s = t
theorem set.image_inter_preimage {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
f '' (s f ⁻¹' t) = f '' s t
theorem set.image_preimage_inter {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
f '' (f ⁻¹' t s) = t f '' s
@[simp]
theorem set.image_inter_nonempty_iff {α : Type u} {β : Type v} {f : α → β} {s : set α} {t : set β} :
(f '' s t).nonempty (s f ⁻¹' t).nonempty
theorem set.image_diff_preimage {α : Type u} {β : Type v} {f : α → β} {s : set α} {t : set β} :
f '' (s \ f ⁻¹' t) = f '' s \ t
theorem set.compl_image {α : Type u} :
theorem set.compl_image_set_of {α : Type u} {p : set α → Prop} :
has_compl.compl '' {s : set α | p s} = {s : set α | p s}
theorem set.inter_preimage_subset {α : Type u} {β : Type v} (s : set α) (t : set β) (f : α → β) :
s f ⁻¹' t f ⁻¹' (f '' s t)
theorem set.union_preimage_subset {α : Type u} {β : Type v} (s : set α) (t : set β) (f : α → β) :
s f ⁻¹' t f ⁻¹' (f '' s t)
theorem set.subset_image_union {α : Type u} {β : Type v} (f : α → β) (s : set α) (t : set β) :
f '' (s f ⁻¹' t) f '' s t
theorem set.preimage_subset_iff {α : Type u} {β : Type v} {A : set α} {B : set β} {f : α → β} :
f ⁻¹' B A ∀ (a : α), f a Ba A
theorem set.image_eq_image {α : Type u} {β : Type v} {s t : set α} {f : α → β} (hf : function.injective f) :
f '' s = f '' t s = t
theorem set.image_subset_image_iff {α : Type u} {β : Type v} {s t : set α} {f : α → β} (hf : function.injective f) :
f '' s f '' t s t
theorem set.prod_quotient_preimage_eq_image {α : Type u} {β : Type v} [s : setoid α] (g : → β) {h : α → β} (Hh : h = ) (r : set × β)) :
{x : | (g x.fst, g x.snd) r} = (λ (a : α × α), (a.fst, a.snd)) '' ((λ (a : α × α), (h a.fst, h a.snd)) ⁻¹' r)
theorem set.exists_image_iff {α : Type u} {β : Type v} (f : α → β) (x : set α) (P : β → Prop) :
(∃ (a : (f '' x)), P a) ∃ (a : x), P (f a)
def set.image_factorization {α : Type u} {β : Type v} (f : α → β) (s : set α) :
s → (f '' s)

Restriction of `f` to `s` factors through `s.image_factorization f : s → f '' s`.

Equations
theorem set.image_factorization_eq {α : Type u} {β : Type v} {f : α → β} {s : set α} :
theorem set.surjective_onto_image {α : Type u} {β : Type v} {f : α → β} {s : set α} :
theorem set.image_perm {α : Type u} {s : set α} {σ : equiv.perm α} (hs : {a : α | σ a a} s) :
σ '' s = s

If the only elements outside `s` are those left fixed by `σ`, then mapping by `σ` has no effect.

### Subsingleton #

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

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

Equations
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} :
@[simp]
theorem set.subsingleton_singleton {α : Type u} {a : α} :
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 sb = a) :
theorem set.subsingleton_iff_singleton {α : Type u} {s : set α} {x : α} (hx : x s) :
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 α] :
@[simp]
theorem set.subsingleton_univ_iff {α : Type u} :
theorem set.subsingleton_of_subsingleton {α : Type u} [subsingleton α] {s : set α} :
theorem set.subsingleton_is_top (α : Type u_1)  :
{x : α | is_top x}.subsingleton
theorem set.subsingleton_is_bot (α : Type u_1)  :
{x : α | is_bot x}.subsingleton
theorem set.exists_eq_singleton_iff_nonempty_subsingleton {α : Type u} {s : set α} :
(∃ (a : α), s = {a})
@[simp, norm_cast]
theorem set.subsingleton_coe {α : Type u} (s : set α) :

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

@[protected, instance]
def set.subsingleton_coe_of_subsingleton {α : Type u} [subsingleton α] {s : set α} :

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

theorem set.subsingleton.image {α : Type u} {β : Type v} {s : set α} (hs : s.subsingleton) (f : α → β) :

The image of a subsingleton is a subsingleton.

theorem set.subsingleton.preimage {α : Type u} {β : Type v} {s : set β} (hs : s.subsingleton) {f : α → β} (hf : function.injective f) :

The preimage of a subsingleton under an injective map is a subsingleton.

theorem set.subsingleton_of_image {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) (s : set α) (hs : (f '' s).subsingleton) :

If the image of a set under an injective map is a subsingleton, the set is a subsingleton.

theorem set.subsingleton_of_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.surjective f) (s : set β) (hs : (f ⁻¹' s).subsingleton) :

If the preimage of a set under an surjective map is a subsingleton, the set is a subsingleton.

### Nontrivial #

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

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

Equations
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
@[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) :
theorem set.nontrivial.mono {α : Type u} {s t : set α} (hs : s.nontrivial) (hst : s t) :
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 α} {z : α} (hs : s.nontrivial) :
∃ (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) :