mathlib documentation

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 coersion 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, image, preimage, pre-image, range, union, intersection, insert, singleton, complement, powerset

Set coercion to a type

@[instance]
def set.has_le {α : Type u_1} :
has_le (set α)

Equations
@[instance]
def set.has_lt {α : Type u_1} :
has_lt (set α)

Equations
@[simp]
theorem set.bot_eq_empty {α : Type u_1} :

@[simp]
theorem set.sup_eq_union {α : Type u_1} (s t : set α) :
s t = s t

@[simp]
theorem set.inf_eq_inter {α : Type u_1} (s t : set α) :
s t = s t

@[simp]
theorem set.le_eq_subset {α : Type u_1} (s t : set α) :
s t = (s t)

@[instance]
def set.has_coe_to_sort {α : Type u_1} :

Coercion from a set to the corresponding subtype.

Equations
theorem set.set_coe_eq_subtype {α : Type u} (s : set α) :
s = {x // x s}

@[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

@[instance]
def set.inhabited {α : Type u} :

Equations
@[ext]
theorem set.ext {α : Type u} {a b : set α} :
(∀ (x : α), x a x b)a = b

theorem set.ext_iff {α : Type u} {s t : set α} :
s = t ∀ (x : α), x s x t

theorem set.mem_of_mem_of_subset {α : Type u} {x : α} {s t : set α} :
x ss tx t

Lemmas about mem and set_of

@[simp]
theorem set.mem_set_of_eq {α : Type u} {a : α} {p : α → Prop} :
a {a : α | p a} = p a

theorem set.nmem_set_of_eq {α : Type u} {a : α} {P : α → Prop} :
a {a : α | P a} = ¬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 α} :
set_of s = 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

@[instance]
def set.decidable_mem {α : Type u} (s : set α) [H : decidable_pred s] (a : α) :

Equations
@[instance]
def set.decidable_set_of {α : Type u} (p : α → Prop) [H : decidable_pred p] :
decidable_pred {a : α | p a}

Equations
@[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}

Lemmas about subsets

theorem set.subset_def {α : Type u} {s t : set α} :
s t = ∀ (x : α), x sx t

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

theorem set.subset.rfl {α : Type u} {s : set α} :
s s

theorem set.subset.trans {α : Type u} {a b c : set α} :
a bb ca c

theorem set.mem_of_eq_of_mem {α : Type u} {x y : α} {s : set α} :
x = yy sx s

theorem set.subset.antisymm {α : Type u} {a b : set α} :
a bb aa = 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 : α} :
s₁ s₂a s₁a 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.

@[instance]
def set.has_ssubset {α : Type u} :

Equations
@[simp]
theorem set.lt_eq_ssubset {α : Type u} (s t : set α) :
s < t = (s t)

theorem set.ssubset_def {α : Type u} {s t : set α} :
s t = (s t ¬t s)

theorem set.eq_or_ssubset_of_subset {α : Type u} {s t : set α} :
s ts = t s t

theorem set.exists_of_ssubset {α : Type u} {s t : set α} :
s t(∃ (x : α) (H : x t), x s)

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 α} :
s t(s t ∃ (x : α) (H : x t), x 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

def set.nonempty {α : Type u} :
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
theorem set.nonempty_def {α : Type u} {s : set α} :
s.nonempty ∃ (x : α), x s

theorem set.nonempty_of_mem {α : Type u} {s : set α} {x : α} :
x s → s.nonempty

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

theorem set.nonempty.ne_empty {α : Type u} {s : set α} :
s.nonemptys

def set.nonempty.some {α : Type u} {s : set α} :
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
theorem set.nonempty.some_mem {α : Type u} {s : set α} (h : s.nonempty) :
h.some s

theorem set.nonempty.mono {α : Type u} {s t : set α} :
s ts.nonempty → t.nonempty

theorem set.nonempty_of_not_subset {α : Type u} {s t : set α} :
¬s t(s \ t).nonempty

theorem set.nonempty_of_ssubset {α : Type u} {s t : set α} :
s t(t \ s).nonempty

theorem set.nonempty.of_diff {α : Type u} {s t : set α} :
(s \ t).nonempty → s.nonempty

theorem set.nonempty_of_ssubset' {α : Type u} {s t : set α} :
s t → t.nonempty

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

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

@[simp]
theorem set.union_nonempty {α : Type u} {s t : set α} :

theorem set.nonempty.left {α : Type u} {s t : set α} :
(s t).nonempty → s.nonempty

theorem set.nonempty.right {α : Type u} {s t : set α} :
(s t).nonempty → t.nonempty

theorem set.nonempty_inter_iff_exists_right {α : Type u} {s t : set α} :
(s t).nonempty ∃ (x : t), x s

theorem set.nonempty_inter_iff_exists_left {α : Type u} {s t : set α} :
(s t).nonempty ∃ (x : s), x t

@[simp]
theorem set.univ_nonempty {α : Type u} [h : nonempty α] :

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

@[simp]
theorem set.nonempty_insert {α : Type u} (a : α) (s : set α) :

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} =

theorem set.eq_empty_iff_forall_not_mem {α : Type u} {s : set α} :
s = ∀ (x : α), x s

@[simp]
theorem set.empty_subset {α : Type u} (s : set α) :

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

theorem set.eq_empty_of_subset_empty {α : Type u} {s : set α} :
s s =

theorem set.eq_empty_of_not_nonempty {α : Type u} (h : ¬nonempty α) (s : set α) :
s =

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

theorem set.empty_not_nonempty {α : Type u} :

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

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

theorem set.subset_eq_empty {α : Type u} {s t : set α} :
t ss = t =

theorem set.ball_empty_iff {α : Type u} {p : α → Prop} :
(∀ (x : α), x p x) true

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 : α) :

theorem set.empty_ne_univ {α : Type u} [h : 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 α} :
s = set.univ ∀ (x : α), x s

theorem set.eq_univ_of_forall {α : Type u} {s : set α} :
(∀ (x : α), x s)s = set.univ

theorem set.eq_univ_of_subset {α : Type u} {s t : set α} :
s ts = set.univt = set.univ

@[simp]
theorem set.univ_eq_empty_iff {α : Type u} :

theorem set.exists_mem_of_nonempty (α : Type u_1) [nonempty α] :
∃ (x : α), x set.univ

@[instance]

Equations
def set.diagonal (α : Type u_1) :
set × α)

diagonal α is the subset of α × α consisting of all pairs of the form (a, a).

Equations
@[simp]
theorem set.mem_diagonal {α : Type u_1} (x : α) :
(x, x) set.diagonal α

Lemmas about union

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 α} :
x a bx a x b

theorem set.mem_union.elim {α : Type u} {x : α} {a b : set α} {P : Prop} :
x a b(x a → P)(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)

@[instance]

@[instance]

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₂

theorem set.union_eq_self_of_subset_left {α : Type u} {s t : set α} :
s ts t = t

theorem set.union_eq_self_of_subset_right {α : Type u} {s t : set α} :
t ss 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 α} :
s rt rs 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 α} :
s₁ s₂t₁ t₂s₁ t₁ s₂ t₂

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

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

@[simp]
theorem set.union_empty_iff {α : Type u} {s t : set α} :
s t = s = t =

Lemmas about intersection

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 α} :
x ax bx a b

theorem set.mem_of_mem_inter_left {α : Type u} {x : α} {a b : set α} :
x a bx a

theorem set.mem_of_mem_inter_right {α : Type u} {x : α} {a b : set α} :
x a bx 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)

@[instance]

@[instance]

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 α} :
r sr tr 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_univ {α : Type u} (a : set α) :

@[simp]
theorem set.univ_inter {α : Type u} (a : set α) :

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

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

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

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_compl_nonempty_iff {α : Type u} {s t : set α} :

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_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_distrib_right {α : Type u} (s t u : set α) :
s t u = (s u) (t u)

Lemmas about insert

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

theorem set.insert_def {α : Type u} (x : α) (s : set α) :
insert x s = {y : α | y = x y s}

@[simp]
theorem set.subset_insert {α : Type u} (x : α) (s : set α) :
s insert x s

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

theorem set.mem_insert_of_mem {α : Type u} {x : α} {s : set α} (y : α) :
x sx insert y s

theorem set.eq_or_mem_of_mem_insert {α : Type u} {x a : α} {s : set α} :
x insert a sx = a x s

theorem set.mem_of_mem_insert_of_ne {α : Type u} {x a : α} {s : set α} :
x insert a sx ax s

@[simp]
theorem set.mem_insert_iff {α : Type u} {x a : α} {s : set α} :
x insert a s x = a x s

@[simp]
theorem set.insert_eq_of_mem {α : Type u} {a : α} {s : set α} :
a sinsert a s = s

theorem set.ne_insert_of_not_mem {α : Type u} {s : set α} (t : set α) {a : α} :
a ss insert a t

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

theorem set.insert_subset_insert {α : Type u} {a : α} {s t : set α} :
s tinsert a s insert a t

theorem set.ssubset_iff_insert {α : Type u} {s t : set α} :
s t ∃ (a : α) (H : a s), insert a s t

theorem set.ssubset_insert {α : Type u} {s : set α} {a : α} :
a ss insert a s

theorem set.insert_comm {α : Type u} (a b : α) (s : set α) :
insert a (insert b s) = insert b (insert a s)

theorem set.insert_union {α : Type u} {a : α} {s t : set α} :
insert a s t = insert a (s t)

@[simp]
theorem set.union_insert {α : Type u} {a : α} {s t : set α} :
s insert a t = insert a (s t)

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

theorem set.insert_inter {α : Type u} (x : α) (s t : set α) :
insert x (s t) = insert x s insert x t

theorem set.forall_of_forall_insert {α : Type u} {P : α → Prop} {a : α} {s : set α} (h : ∀ (x : α), x insert a sP x) (x : α) :
x sP x

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

theorem set.bex_insert_iff {α : Type u} {P : α → Prop} {a : α} {s : set α} :
(∃ (x : α) (H : x insert a s), P x) (∃ (x : α) (H : x s), P x) P a

theorem set.ball_insert_iff {α : Type u} {P : α → Prop} {a : α} {s : set α} :
(∀ (x : α), x insert a sP x) P a ∀ (x : α), x sP x

Lemmas about singletons

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

theorem set.eq_of_mem_singleton {α : Type u} {x y : α} :
x {y}x = y

@[simp]
theorem set.singleton_eq_singleton_iff {α : Type u} {x y : α} :
{x} = {y} x = y

theorem set.mem_singleton_of_eq {α : Type u} {x y : α} :
x = yx {y}

theorem set.insert_eq {α : Type u} (x : α) (s : set α) :
insert x s = {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 = insert a s

@[simp]
theorem set.union_singleton {α : Type u} {a : α} {s : set α} :
s {a} = insert a s

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

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

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

@[instance]
def set.unique_singleton {α : Type u} (a : α) :

Equations
theorem set.eq_singleton_iff_unique_mem {α : Type u} {s : set α} {a : α} :
s = {a} a s ∀ (x : α), x sx = a

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

theorem set.mem_sep {α : Type u} {s : set α} {p : α → Prop} {x : α} :
x sp xx {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 α} :
s ts = {x ∈ t | x s}

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

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}

Lemmas about complement

theorem set.mem_compl {α : Type u} {s : set α} {x : α} :
x sx 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 : α} :
x sx 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

@[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_compl {α : Type u} (s : set α) :

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

@[simp]
theorem set.compl_univ {α : Type u} :

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

theorem set.compl_univ_iff {α : 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}

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_comp_compl {α : Type u} :

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

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

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

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

theorem set.subset_compl_iff_disjoint {α : Type u} {s t : set α} :
s t s t =

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

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 : α} :
x sx tx s \ t

theorem set.mem_of_mem_diff {α : Type u} {s t : set α} {x : α} :
x s \ tx s

theorem set.not_mem_of_mem_diff {α : Type u} {s t : set α} {x : α} :
x s \ tx 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.union_diff_cancel' {α : Type u} {s t u : set α} :
s tt ut u \ s = u

theorem set.union_diff_cancel {α : Type u} {s t : set α} :
s ts t \ s = t

theorem set.union_diff_cancel_left {α : Type u} {s t : set α} :
s t (s t) \ s = t

theorem set.union_diff_cancel_right {α : Type u} {s t : set α} :
s t (s t) \ t = s

theorem set.union_diff_left {α : Type u} {s t : set α} :
(s t) \ s = t \ s

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

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

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

theorem set.union_inter_distrib_right {α : 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)

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

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

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

theorem set.diff_subset {α : Type u} (s t : set α) :
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 α} :
s₁ s₂s₁ \ t s₂ \ t

theorem set.diff_subset_diff_right {α : Type u} {s t u : set α} :
t us \ u s \ t

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

@[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

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

@[simp]
theorem set.diff_singleton_subset_iff {α : Type u} {x : α} {s t : set α} :
s \ {x} t s insert x t

theorem set.subset_diff_singleton {α : Type u} {x : α} {s t : set α} :
s tx ss t \ {x}

theorem set.subset_insert_diff_singleton {α : Type u} (x : α) (s : set α) :
s insert x (s \ {x})

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

theorem set.diff_inter {α : Type u} {s t u : set α} :
s \ (t u) = s \ t s \ u

theorem set.diff_inter_diff {α : Type u} {s t u : set α} :
s \ t (s \ u) = s \ (t u)

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

theorem set.diff_diff_right {α : Type u} {s t u : set α} :
s \ (t \ u) = s \ t s u

@[simp]
theorem set.insert_diff_of_mem {α : Type u} {a : α} {t : set α} (s : set α) :
a tinsert a s \ t = s \ t

theorem set.insert_diff_of_not_mem {α : Type u} {a : α} {t : set α} (s : set α) :
a tinsert a s \ t = insert a (s \ t)

theorem set.insert_diff_self_of_not_mem {α : Type u} {a : α} {s : set α} :
a sinsert a s \ {a} = s

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

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

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

theorem set.diff_inter_self_eq_diff {α : Type u} {s t : set α} :
s \ (t s) = s \ t

theorem set.diff_self_inter {α : Type u} {s t : set α} :
s \ (s t) = s \ t

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 α} :
a ss \ {a} = s

@[simp]
theorem set.insert_diff_singleton {α : Type u} {a : α} {s : set α} :
insert a (s \ {a}) = insert a s

@[simp]
theorem set.diff_self {α : Type u} {s : set α} :
s \ s =

theorem set.diff_diff_cancel_left {α : Type u} {s t : set α} :
s tt \ (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

Powerset

theorem set.mem_powerset {α : Type u} {x s : set α} :
x sx 𝒫s

theorem set.subset_of_mem_powerset {α : Type u} {x s : set α} :
x 𝒫sx 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 α} :

@[simp]
theorem set.powerset_nonempty {α : Type u} {s : set α} :

@[simp]
theorem set.powerset_empty {α : Type u} :

Inverse image

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

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

Equations
@[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 β} :
(∀ (x : α), f x = g x)f ⁻¹' s = g ⁻¹' s

theorem set.preimage_mono {α : Type u} {β : Type v} {f : α → β} {s t : set β} :
s tf ⁻¹' 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 α} :

@[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_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 α} :
id ⁻¹' s = s

@[simp]
theorem set.preimage_id' {α : Type u} {s : set α} :
(λ (x : α), x) ⁻¹' s = s

theorem set.preimage_const_of_mem {α : Type u} {β : Type v} {b : β} {s : set β} :
b s(λ (x : α), b) ⁻¹' s = set.univ

theorem set.preimage_const_of_not_mem {α : Type u} {β : Type v} {b : β} {s : set β} :
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 = subtype.val ⁻¹' t ∀ (x : α) (h : p x), x, h⟩ s x t

Image of a set under a function

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 α} :
x af x f '' a

theorem set.mem_image_of_injective {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} :
function.injective f(f a f '' s a s)

theorem set.ball_image_of_ball {α : Type u} {β : Type v} {f : α → β} {s : set α} {p : β → Prop} (h : ∀ (x : α), x sp (f x)) (y : β) :
y f '' sp y

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.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 : β} :
y f '' s(∀ (x : α), x sC (f x))C y

theorem set.image_congr {α : Type u} {β : Type v} {f g : α → β} {s : set α} :
(∀ (a : α), a sf a = g a)f '' s = g '' s

theorem set.image_congr' {α : Type u} {β : Type v} {f g : α → β} {s : set α} :
(∀ (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_subset {α : Type u} {β : Type v} {a b : set α} (f : α → β) :
a bf '' 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 α} :
(∀ (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 α} :
function.injective ff '' s f '' t = f '' (s t)

theorem set.image_univ_of_surjective {β : Type v} {ι : Type u_1} {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.inter_singleton_nonempty {α : Type u} {s : set α} {a : α} :
(s {a}).nonempty a s

theorem set.mem_compl_image {α : Type u} (t : set α) (S : set (set α)) :

@[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 (set α)) :
compl '' (compl '' S) = S

theorem set.image_insert_eq {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} :
f '' insert a s = 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 : function.left_inverse g f) (s : set α) :
f '' s g ⁻¹' s

theorem set.preimage_subset_image_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} (I : function.left_inverse g f) (s : set β) :
f ⁻¹' s g '' s

theorem set.image_eq_preimage_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} :

theorem set.mem_image_iff_of_inverse {α : Type u} {β : Type v} {f : α → β} {g : β → α} {b : β} {s : set α} :

theorem set.image_compl_subset {α : Type u} {β : Type v} {f : α → β} {s : set α} :

theorem set.subset_image_compl {α : Type u} {β : Type v} {f : α → β} {s : set α} :

theorem set.image_compl_eq {α : Type u} {β : Type v} {f : α → β} {s : set α} :

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 α} :

@[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 α) :
function.injective ff ⁻¹' (f '' s) = s

theorem set.image_preimage_eq {α : Type u} {β : Type v} {f : α → β} {s : set β} :
function.surjective ff '' (f ⁻¹' s) = s

theorem set.preimage_eq_preimage {α : Type u} {β : Type v} {s t : set α} {f : β → α} :
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

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_set_of {α : Type u} {p : set α → Prop} :
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 : α → β} :
function.injective f(f '' s = f '' t s = t)

theorem set.image_subset_image_iff {α : Type u} {β : Type v} {s t : set α} {f : α → β} :
function.injective f(f '' s f '' t s t)

theorem set.prod_quotient_preimage_eq_image {α : Type u} {β : Type v} [s : setoid α] (g : quotient s → β) {h : α → β} (Hh : h = g quotient.mk) (r : set × β)) :
{x : quotient s × quotient s | (g x.fst, g x.snd) r} = (λ (a : α × α), (a.fst, a.snd)) '' ((λ (a : α × α), (h a.fst, h a.snd)) ⁻¹' r)

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 α} :

Subsingleton

def set.subsingleton {α : Type u} :
set α → Prop

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

Equations
theorem set.subsingleton.mono {α : Type u} {s t : set α} :
t.subsingletons t → s.subsingleton

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

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

theorem set.subsingleton_empty {α : Type u} :

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

theorem set.subsingleton.eq_empty_or_singleton {α : Type u} {s : set α} :
s.subsingleton(s = ∃ (x : α), s = {x})

@[simp]
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.

Lemmas about range of a function.

def set.range {α : Type u} {ι : Sort x} :
(ι → α)set α

Range of a function.

This function is more flexible than f '' univ, as the image requires that the domain is in Type and not an arbitrary Sort.

Equations
@[simp]
theorem set.mem_range {α : Type u} {ι : Sort x} {f : ι → α} {x : α} :
x set.range f ∃ (y : ι), f y = x

@[simp]
theorem set.mem_range_self {α : Type u} {ι : Sort x} {f : ι → α} (i : ι) :

theorem set.forall_range_iff {α : Type u} {ι : Sort x} {f : ι → α} {p : α → Prop} :
(∀ (a : α), a set.range fp a) ∀ (i : ι), p (f i)

theorem set.exists_range_iff {α : Type u} {ι : Sort x} {f : ι → α} {p : α → Prop} :
(∃ (a : α) (H : a set.range f), p a) ∃ (i : ι), p (f i)

theorem set.exists_range_iff' {α : Type u} {ι : Sort x} {f : ι → α} {p : α → Prop} :
(∃ (a : α), a set.range f p a) ∃ (i : ι), p (f i)

theorem set.range_iff_surjective {α : Type u} {ι : Sort x} {f : ι → α} :

@[simp]
theorem set.range_id {α : Type u} :

@[simp]
theorem set.range_quot_mk {α : Type u} (r : α → α → Prop) :
set.range (quot.mk r) = set.univ

@[simp]
theorem set.image_univ {β : Type v} {ι : Type u_1} {f : ι → β} :

theorem set.image_subset_range {β : Type v} {ι : Type u_1} (f : ι → β) (s : set ι) :

theorem set.range_comp {α : Type u} {β : Type v} {ι : Sort x} (g : α → β) (f : ι → α) :

theorem set.range_subset_iff {α : Type u} {ι : Sort x} {f : ι → α} {s : set α} :
set.range f s ∀ (y : ι), f y s

theorem set.range_comp_subset_range {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) :

theorem set.range_nonempty_iff_nonempty {α : Type u} {ι : Sort x} {f : ι → α} :

theorem set.range_nonempty {α : Type u} {ι : Sort x} [h : nonempty ι] (f : ι → α) :

@[simp]
theorem set.range_eq_empty {α : Type u} {ι : Sort x} {f : ι → α} :

@[simp]
theorem set.image_union_image_compl_eq_range {α : Type u} {β : Type v} {s : set α} (f : α → β) :
f '' s f '' s = set.range f

theorem set.image_preimage_eq_inter_range {α : Type u} {β : Type v} {f : α → β} {t : set β} :
f '' (f ⁻¹' t) = t set.range f

theorem set.image_preimage_eq_of_subset {α : Type u} {β : Type v} {f : α → β} {s : set β} :
s set.range ff '' (f ⁻¹' s) = s

theorem set.image_preimage_eq_iff {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f '' (f ⁻¹' s) = s s set.range f

theorem set.preimage_subset_preimage_iff {α : Type u} {β : Type v} {s t : set α} {f : β → α} :
s set.range f(f ⁻¹' s f ⁻¹' t s t)

theorem set.preimage_eq_preimage' {α : Type u} {β : Type v} {s t : set α} {f : β → α} :
s set.range ft set.range f(f ⁻¹' s = f ⁻¹' t s = t)

@[simp]
theorem set.preimage_inter_range {α : Type u} {β : Type v} {f : α → β} {s : set β} :

@[simp]
theorem set.preimage_range_inter {α : Type u} {β : Type v} {f : α → β} {s : set β} :

theorem set.preimage_image_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s

@[simp]
theorem set.quot_mk_range_eq {α : Type u} [setoid α] :
set.range (λ (x : α), x) = set.univ

theorem set.range_const_subset {α : Type u} {ι : Sort x} {c : α} :
set.range (λ (x : ι), c) {c}

@[simp]
theorem set.range_const {α : Type u} {ι : Sort x} [nonempty ι] {c : α} :
set.range (λ (x : ι), c) = {c}

theorem set.diagonal_eq_range {α : Type u_1} :
set.diagonal α = set.range (λ (x : α), (x, x))

theorem set.preimage_singleton_nonempty {α : Type u} {β : Type v} {f : α → β} {y : β} :

theorem set.preimage_singleton_eq_empty {α : Type u} {β : Type v} {f : α → β} {y : β} :

theorem set.range_subset_singleton {α : Type u} {ι : Sort x} {f : ι → α} {x : α} :

theorem set.image_compl_preimage {α : Type u} {β : Type v} {f : α → β} {s : set β} :
f '' (f ⁻¹' s) = set.range f \ s

@[simp]
theorem set.range_sigma_mk {α : Type u} {β : α → Type u_1} (a : α) :

def set.range_factorization {β : Type v} {ι : Sort x} (f : ι → β) :
ι → (set.range f)

Any map f : ι → β factors through a map range_factorization f : ι → range f.

Equations
theorem set.range_factorization_eq {β : Type v} {ι : Sort x} {f : ι → β} :

theorem set.surjective_onto_range {α : Type u} {ι : Sort x} {f : ι → α} :

theorem set.image_eq_range {α : Type u} {β : Type v} (f : α → β) (s : set α) :
f '' s = set.range (λ (x : s), f x)

@[simp]
theorem set.sum.elim_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ) (g : β → γ) :

theorem set.range_ite_subset' {α : Type u} {β : Type v} {p : Prop} [decidable p] {f g : α → β} :

theorem set.range_ite_subset {α : Type u} {β : Type v} {p : α → Prop} [decidable_pred p] {f g : α → β} :
set.range (λ (x : α), ite (p x) (f x) (g x)) set.range f set.range g

@[simp]
theorem set.preimage_range {α : Type u} {β : Type v} (f : α → β) :

theorem set.range_unique {α : Type u} {ι : Sort x} {f : ι → α} [h : unique ι] :
set.range f = {f (default ι)}

The range of a function from a unique type contains just the function applied to its single value.

def set.pairwise_on {α : Type u} :
set α(α → α → Prop) → Prop

The set s is pairwise r if r x y for all distinct x y ∈ s.

Equations
theorem set.pairwise_on.mono {α : Type u} {s t : set α} {r : α → α → Prop} :
t ss.pairwise_on rt.pairwise_on r

theorem set.pairwise_on.mono' {α : Type u} {s : set α} {r r' : α → α → Prop} :
(∀ (a b : α), r a br' a b)s.pairwise_on rs.pairwise_on r'

theorem set.pairwise_on_eq_iff_exists_eq {α : Type u} {β : Type v} [nonempty β] (s : set α) (f : α → β) :
s.pairwise_on (λ (x y : α), f x = f y) ∃ (z : β), ∀ (x : α), x sf x = z

If and only if f takes pairwise equal values on s, there is some value it takes everywhere on s.

theorem function.surjective.preimage_injective {α : Type u_2} {β : Type u_3} {f : α → β} :

theorem function.injective.preimage_surjective {α : Type u_2} {β : Type u_3} {f : α → β} :

theorem function.surjective.image_surjective {α : Type u_2} {β : Type u_3} {f : α → β} :

theorem function.injective.image_injective {α : Type u_2} {β : Type u_3} {f : α → β} :

theorem function.surjective.preimage_subset_preimage_iff {α : Type u_2} {β : Type u_3} {f : α → β} {s t : set β} :

theorem function.surjective.range_comp {ι : Sort u_1} {α : Type u_2} {ι' : Sort u_3} {f : ι → ι'} (hf : function.surjective f) (g : ι' → α) :

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

Image and preimage on subtypes

theorem subtype.coe_image {α : Type u_1} {p : α → Prop} {s : set (subtype p)} :
coe '' s = {x : α | ∃ (h : p x), x, h⟩ s}

theorem subtype.range_coe {α : Type u_1} {s : set α} :

theorem subtype.range_val {α : Type u_1} {s : set α} :

A variant of range_coe. Try to use range_coe if possible. This version is useful when defining a new type that is defined as the subtype of something. In that case, the coercion doesn't fire anymore.

@[simp]
theorem subtype.range_coe_subtype {α : Type u_1} {p : α → Prop} :
set.range coe = {x : α | p x}

We make this the simp lemma instead of range_coe. The reason is that if we write for s : set α the function coe : s → α, then the inferred implicit arguments of coe are coe α (λ x, x ∈ s).

@[simp]
theorem subtype.coe_preimage_self {α : Type u_1} (s : set α) :

theorem subtype.range_val_subtype {α : Type u_1} {p : α → Prop} :
set.range subtype.val = {x : α | p x}

theorem subtype.coe_image_subset {α : Type u_1} (s : set α) (t : set s) :
coe '' t s

theorem subtype.coe_image_univ {α : Type u_1} (s : set α) :

@[simp]
theorem subtype.image_preimage_coe {α : Type u_1} (s t : set α) :
coe '' (coe ⁻¹' t) = t s

theorem subtype.image_preimage_val {α : Type u_1} (s t : set α) :

theorem subtype.preimage_coe_eq_preimage_coe_iff {α : Type u_1} {s t u : set α} :
coe ⁻¹' t = coe ⁻¹' u t s = u s

theorem subtype.preimage_val_eq_preimage_val_iff {α : Type u_1} (s t u : set α) :

theorem subtype.exists_set_subtype {α : Type u_1} {t : set α} (p : set α → Prop) :
(∃ (s : set t), p (coe '' s)) ∃ (s : set α), s t p s

theorem subtype.preimage_coe_nonempty {α : Type u_1} {s t : set α} :

Lemmas about cartesian product of sets

def set.prod {α : Type u_1} {β : Type u_2} :
set αset βset × β)

The cartesian product prod s t is the set of (a, b) such that a ∈ s and b ∈ t.

Equations
theorem set.prod_eq {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :

theorem set.mem_prod_eq {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β} :
p s.prod t = (p.fst s p.snd t)

@[simp]
theorem set.mem_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β} :
p s.prod t p.fst s p.snd t

@[simp]
theorem set.prod_mk_mem_set_prod_eq {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} {b : β} :
(a, b) s.prod t = (a s b t)

theorem set.mk_mem_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} {b : β} :
a sb t(a, b) s.prod t

theorem set.prod_mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : set α} {t₁ t₂ : set β} :
s₁ s₂t₁ t₂s₁.prod t₁ s₂.prod t₂

theorem set.prod_subset_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {P : set × β)} :
s.prod t P ∀ (x : α), x s∀ (y : β), y t(x, y) P

theorem set.forall_prod_set {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β → Prop} :
(∀ (x : α × β), x s.prod tp x) ∀ (x : α), x s∀ (y : β), y tp (x, y)

theorem set.exists_prod_set {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β → Prop} :
(∃ (x : α × β) (H : x s.prod t), p x) ∃ (x : α) (H : x s) (y : β) (H : y t), p (x, y)

@[simp]
theorem set.prod_empty {α : Type u_1} {β : Type u_2} {s : set α} :

@[simp]
theorem set.empty_prod {α : Type u_1} {β : Type u_2} {t : set β} :

@[simp]
theorem set.univ_prod_univ {α : Type u_1} {β : Type u_2} :

theorem set.univ_prod {α : Type u_1} {β : Type u_2} {t : set β} :

theorem set.prod_univ {α : Type u_1} {β : Type u_2} {s : set α} :

@[simp]
theorem set.singleton_prod {α : Type u_1} {β : Type u_2} {t : set β} {a : α} :
{a}.prod t = prod.mk a '' t

@[simp]
theorem set.prod_singleton {α : Type u_1} {β : Type u_2} {s : set α} {b : β} :
s.prod {b} = (λ (a : α), (a, b)) '' s

theorem set.singleton_prod_singleton {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
{a}.prod {b} = {(a, b)}

@[simp]
theorem set.union_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : set α} {t : set β} :
(s₁ s₂).prod t = s₁.prod t s₂.prod t

@[simp]
theorem set.prod_union {α : Type u_1} {β : Type u_2} {s : set α} {t₁ t₂ : set β} :
s.prod (t₁ t₂) = s.prod t₁ s.prod t₂

theorem set.prod_inter_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : set α} {t₁ t₂ : set β} :
s₁.prod t₁ s₂.prod t₂ = (s₁ s₂).prod (t₁ t₂)

theorem set.insert_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} :
(insert a s).prod t = prod.mk a '' t s.prod t

theorem set.prod_insert {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {b : β} :
s.prod (insert b t) = (λ (a : α), (a, b)) '' s s.prod t

theorem set.prod_preimage_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : set α} {t : set β} {f : γ → α} {g : δ → β} :
(f ⁻¹' s).prod (g ⁻¹' t) = (λ (p : γ × δ), (f p.fst, g p.snd)) ⁻¹' s.prod t

@[simp]
theorem set.mk_preimage_prod_left {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {y : β} :
y t(λ (x : α), (x, y)) ⁻¹' s.prod t = s

@[simp]
theorem set.mk_preimage_prod_right {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {x : α} :
x sprod.mk x ⁻¹' s.prod t = t

@[simp]
theorem set.mk_preimage_prod_left_eq_empty {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {y : β} :
y t(λ (x : α), (x, y)) ⁻¹' s.prod t =

@[simp]
theorem set.mk_preimage_prod_right_eq_empty {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {x : α} :
x sprod.mk x ⁻¹' s.prod t =

theorem set.mk_preimage_prod_left_eq_if {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {y : β} [decidable_pred (λ (_x : β), _x t)] :
(λ (x : α), (x, y)) ⁻¹' s.prod t = ite (y t) s

theorem set.mk_preimage_prod_right_eq_if {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {x : α} [decidable_pred (λ (_x : α), _x s)] :
prod.mk x ⁻¹' s.prod t = ite (x s) t

theorem set.preimage_swap_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :

theorem set.image_swap_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :

theorem set.prod_image_image_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : set α} {t : set β} {m₁ : α → γ} {m₂ : β → δ} :
(m₁ '' s).prod (m₂ '' t) = (λ (p : α × β), (m₁ p.fst, m₂ p.snd)) '' s.prod t

theorem set.prod_range_range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ} :
(set.range m₁).prod (set.range m₂) = set.range (λ (p : α × β), (m₁ p.fst, m₂ p.snd))

theorem set.prod_range_univ_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m₁ : α → γ} :
(set.range m₁).prod set.univ = set.range (λ (p : α × β), (m₁ p.fst, p.snd))

theorem set.prod_univ_range_eq {α : Type u_1} {β : Type u_2} {δ : Type u_3} {m₂ : β → δ} :
set.univ.prod (set.range m₂) = set.range (λ (p : α × β), (p.fst, m₂ p.snd))

theorem set.nonempty.prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s.nonemptyt.nonempty(s.prod t).nonempty

theorem set.nonempty.fst {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s.prod t).nonempty → s.nonempty

theorem set.nonempty.snd {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s.prod t).nonempty → t.nonempty

theorem set.prod_nonempty_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :

theorem set.prod_eq_empty_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s.prod t = s = t =

theorem set.prod_sub_preimage_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {t : set β} {W : set γ} {f : α × β → γ} :
s.prod t f ⁻¹' W ∀ (a : α) (b : β), a sb tf (a, b) W

theorem set.fst_image_prod_subset {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :

theorem set.prod_subset_preimage_fst {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :

theorem set.fst_image_prod {α : Type u_1} {β : Type u_2} (s : set β) {t : set α} :
t.nonemptyprod.fst '' s.prod t = s

theorem set.snd_image_prod_subset {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :

theorem set.prod_subset_preimage_snd {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :

theorem set.snd_image_prod {α : Type u_1} {β : Type u_2} {s : set α} (hs : s.nonempty) (t : set β) :

theorem set.prod_subset_prod_iff {α : Type u_1} {β : Type u_2} {s s₁ : set α} {t t₁ : set β} :
s.prod t s₁.prod t₁ s s₁ t t₁ s = t =

A product set is included in a product set if and only factors are included, or a factor of the first set is empty.

Lemmas about set-indexed products of sets

def set.pi {ι : Type u_1} {α : ι → Type u_2} :
set ι(Π (i : ι), set (α i))set (Π (i : ι), α i)

Given an index set i and a family of sets s : Π i, set (α i), pi i s is the set of dependent functions f : Πa, π a such that f a belongs to π a whenever a ∈ i.

Equations
  • s.pi t = {f : Π (i : ι), α i | ∀ (i : ι), i sf i t i}
@[simp]
theorem set.mem_pi {ι : Type u_1} {α : ι → Type u_2} {s : set ι} {t : Π (i : ι), set (α i)} {f : Π (i : ι), α i} :
f s.pi t ∀ (i : ι), i sf i t i

@[simp]
theorem set.mem_univ_pi {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} {f : Π (i : ι), α i} :
f set.univ.pi t ∀ (i : ι), f i t i

@[simp]
theorem set.empty_pi {ι : Type u_1} {α : ι → Type u_2} (s : Π (i : ι), set (α i)) :

theorem set.pi_eq_empty {ι : Type u_1} {α : ι → Type u_2} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} :
i st i = s.pi t =

theorem set.univ_pi_eq_empty {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} {i : ι} :
t i = set.univ.pi t =

theorem set.pi_nonempty_iff {ι : Type u_1} {α : ι → Type u_2} {s : set ι} {t : Π (i : ι), set (α i)} :
(s.pi t).nonempty ∀ (i : ι), ∃ (x : α i), i sx t i

theorem set.univ_pi_nonempty_iff {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} :
(set.univ.pi t).nonempty ∀ (i : ι), (t i).nonempty

theorem set.pi_eq_empty_iff {ι : Type u_1} {α : ι → Type u_2} {s : set ι} {t : Π (i : ι), set (α i)} :
s.pi t = ∃ (i : ι), (α ifalse) i s t i =

theorem set.univ_pi_eq_empty_iff {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} :
set.univ.pi t = ∃ (i : ι), t i =

@[simp]
theorem set.insert_pi {ι : Type u_1} {α : ι → Type u_2} (i : ι) (s : set ι) (t : Π (i : ι), set (α i)) :
(insert i s).pi t = function.eval i ⁻¹' t i s.pi t

@[simp]
theorem set.singleton_pi {ι : Type u_1} {α : ι → Type u_2} (i : ι) (t : Π (i : ι), set (α i)) :
{i}.pi t = function.eval i ⁻¹' t i

theorem set.pi_if {ι : Type u_1} {α : ι → Type u_2} {p : ι → Prop} [h : decidable_pred p] (s : set ι) (t₁ t₂ : Π (i : ι), set (α i)) :
s.pi (λ (i : ι), ite (p i) (t₁ i) (t₂ i)) = {i ∈ s | p i}.pi t₁