# Basic definitions about sets #

In this file we define various operations on sets. We also provide basic lemmas needed to unfold the definitions. More advanced theorems about these definitions are located in other files in Mathlib/Data/Set.

## Main definitions #

• complement of a set and set difference;
• Set.Elem: coercion of a set to a type; it is reducibly equal to {x // x ∈ s};
• Set.preimage f s, a.k.a. f ⁻¹' s: preimage of a set;
• Set.range f: the range of a function; it is more general than f '' univ because it allows functions from Sort*;
• s ×ˢ t: product of s : Set α and t : Set β as a set in α × β;
• Set.diagonal: the diagonal in α × α;
• Set.offDiag s: the part of s ×ˢ s that is off the diagonal;
• Set.pi: indexed product of a family of sets ∀ i, Set (α i), as a set in ∀ i, α i;
• Set.EqOn f g s: the predicate saying that two functions are equal on a set;
• Set.MapsTo f s t: the predicate syaing that f sends all points of s to t;
• Set.MapsTo.restrict: restrict f : α → β to f' : s → t provided that Set.MapsTo f s t;
• Set.restrictPreimage: restrict f : α → β to f' : (f ⁻¹' t) → t;
• Set.InjOn: the predicate saying that f is injective on a set;
• Set.SurjOn f s t: the prediate saying that t ⊆ f '' s;
• Set.BijOn f s t: the predicate saying that f is injective on s and f '' s = t;
• Set.graphOn: the graph of a function on a set;
• Set.LeftInvOn, Set.RightInvOn, Set.InvOn: the predicates saying that f' is a left, right or two-sided inverse of f on s, t, or both;
• Set.image2: the image of a pair of sets under a binary operation, mostly useful to define pointwise algebraic operations on sets;
• Set.seq: monadic seq operation on sets; we don't use monadic notation to ensure support for maps between different universes;

## Notations #

• f '' s: image of a set;
• f ⁻¹' s: preimage of a set;
• s ×ˢ t: the product of sets;
• s ∪ t: the union of two sets;
• s ∩ t: the intersection of two sets;
• sᶜ: the complement of a set;
• s \ t: the difference of two sets.

## Keywords #

set, image, preimage

@[simp]
theorem Set.mem_setOf_eq {α : Type u} {x : α} {p : αProp} :
(x {y : α | p y}) = p x
@[simp]
theorem Set.mem_univ {α : Type u} (x : α) :
x Set.univ
instance Set.instHasCompl {α : Type u} :
Equations
• Set.instHasCompl = { compl := fun (s : Set α) => {x : α | ¬x s} }
@[simp]
theorem Set.mem_compl_iff {α : Type u} (s : Set α) (x : α) :
x s ¬x s
theorem Set.diff_eq {α : Type u} (s : Set α) (t : Set α) :
s \ t = s t
@[simp]
theorem Set.mem_diff {α : Type u} {s : Set α} {t : Set α} (x : α) :
x s \ t x s ¬x t
theorem Set.mem_diff_of_mem {α : Type u} {s : Set α} {t : Set α} {x : α} (h1 : x s) (h2 : ¬x t) :
x s \ t
@[reducible]
def Set.Elem {α : Type u} (s : Set α) :

Given the set s, Elem s is the Type of element of s.

Equations
• s = { x : α // x s }
Instances For
instance Set.instCoeSortType {α : Type u} :
CoeSort (Set α) (Type u)

Coercion from a set to the corresponding subtype.

Equations
• Set.instCoeSortType = { coe := Set.Elem }
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

f ⁻¹' t denotes the preimage of t : Set β under the function f : α → β.

Equations
Instances For
@[simp]
theorem Set.mem_preimage {α : Type u} {β : Type v} {f : αβ} {s : Set β} {a : α} :
a f ⁻¹' s f a s

f '' s denotes the image of s : Set α under the function f : α → β.

Equations
Instances For
@[simp]
theorem Set.mem_image {α : Type u} {β : Type v} (f : αβ) (s : Set α) (y : β) :
y f '' s ∃ (x : α), x s f x = y
theorem Set.mem_image_of_mem {α : Type u} {β : Type v} (f : αβ) {x : α} {a : Set α} (h : x a) :
f x f '' a
def Set.imageFactorization {α : Type u} {β : Type v} (f : αβ) (s : Set α) :
s(f '' s)

Restriction of f to s factors through s.imageFactorization f : s → f '' s.

Equations
• = f p,
Instances For
def Set.kernImage {α : Type u} {β : Type v} (f : αβ) (s : Set α) :
Set β

kernImage f s is the set of y such that f ⁻¹ y ⊆ s.

Equations
• = {y : β | ∀ ⦃x : α⦄, f x = yx s}
Instances For
theorem Set.subset_kernImage_iff {α : Type u} {β : Type v} {s : Set β} {t : Set α} {f : αβ} :
s f ⁻¹' s t
def Set.range {α : Type u} {ι : Sort u_1} (f : ια) :
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
• = {x : α | ∃ (y : ι), f y = x}
Instances For
@[simp]
theorem Set.mem_range {α : Type u} {ι : Sort u_1} {f : ια} {x : α} :
x ∃ (y : ι), f y = x
theorem Set.mem_range_self {α : Type u} {ι : Sort u_1} {f : ια} (i : ι) :
f i
def Set.rangeFactorization {α : Type u} {ι : Sort u_1} (f : ια) :
ι()

Any map f : ι → α factors through a map rangeFactorization f : ι → range f.

Equations
• = f i,
Instances For
noncomputable def Set.rangeSplitting {α : Type u} {β : Type v} (f : αβ) :
()α

We can use the axiom of choice to pick a preimage for every element of range f.

Equations
Instances For
theorem Set.apply_rangeSplitting {α : Type u} {β : Type v} (f : αβ) (x : ()) :
f () = x
@[simp]
theorem Set.comp_rangeSplitting {α : Type u} {β : Type v} (f : αβ) :
= Subtype.val
def Set.prod {α : Type u} {β : Type v} (s : Set α) (t : Set β) :
Set (α × β)

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

Equations
Instances For
@[defaultInstance 1000]
instance Set.instSProd {α : Type u} {β : Type v} :
SProd (Set α) (Set β) (Set (α × β))
Equations
• Set.instSProd = { sprod := Set.prod }
theorem Set.prod_eq {α : Type u} {β : Type v} (s : Set α) (t : Set β) :
s ×ˢ t = Prod.fst ⁻¹' s Prod.snd ⁻¹' t
theorem Set.mem_prod_eq {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β} :
(p s ×ˢ t) = (p.fst s p.snd t)
@[simp]
theorem Set.mem_prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β} :
p s ×ˢ t p.fst s p.snd t
theorem Set.prod_mk_mem_set_prod_eq {α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β} :
((a, b) s ×ˢ t) = (a s b t)
theorem Set.mk_mem_prod {α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β} (ha : a s) (hb : b t) :
(a, b) s ×ˢ t
def Set.diagonal (α : Type u_1) :
Set (α × α)

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

Equations
• = {p : α × α | p.fst = p.snd}
Instances For
theorem Set.mem_diagonal {α : Type u} (x : α) :
(x, x)
@[simp]
theorem Set.mem_diagonal_iff {α : Type u} {x : α × α} :
x.fst = x.snd
def Set.offDiag {α : Type u} (s : Set α) :
Set (α × α)

The off-diagonal of a set s is the set of pairs (a, b) with a, b ∈ s and a ≠ b.

Equations
Instances For
@[simp]
theorem Set.mem_offDiag {α : Type u} {x : α × α} {s : Set α} :
x s.offDiag x.fst s x.snd s x.fst x.snd
def Set.pi {ι : Type u_1} {α : ιType u_2} (s : Set ι) (t : (i : ι) → Set (α i)) :
Set ((i : ι) → α i)

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

Equations
• s.pi t = {f : (i : ι) → α i | ∀ (i : ι), i sf i t i}
Instances For
@[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
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
def Set.EqOn {α : Type u} {β : Type v} (f₁ : αβ) (f₂ : αβ) (s : Set α) :

Two functions f₁ f₂ : α → β are equal on s if f₁ x = f₂ x for all x ∈ s.

Equations
• Set.EqOn f₁ f₂ s = ∀ ⦃x : α⦄, x sf₁ x = f₂ x
Instances For
def Set.MapsTo {α : Type u} {β : Type v} (f : αβ) (s : Set α) (t : Set β) :

MapsTo f a b means that the image of a is contained in b.

Equations
Instances For
theorem Set.mapsTo_image {α : Type u} {β : Type v} (f : αβ) (s : Set α) :
Set.MapsTo f s (f '' s)
theorem Set.mapsTo_preimage {α : Type u} {β : Type v} (f : αβ) (t : Set β) :
Set.MapsTo f (f ⁻¹' t) t
def Set.MapsTo.restrict {α : Type u} {β : Type v} (f : αβ) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) :
st

Given a map f sending s : Set α into t : Set β, restrict domain of f to s and the codomain to t. Same as Subtype.map.

Equations
Instances For
@[simp]
theorem Set.restrictPreimage_coe {α : Type u} {β : Type v} (t : Set β) (f : αβ) :
∀ (a : (f ⁻¹' t)), (t.restrictPreimage f a) = f a
def Set.restrictPreimage {α : Type u} {β : Type v} (t : Set β) (f : αβ) :
(f ⁻¹' t)t

The restriction of a function onto the preimage of a set.

Equations
Instances For
def Set.InjOn {α : Type u} {β : Type v} (f : αβ) (s : Set α) :

f is injective on a if the restriction of f to a is injective.

Equations
• = ∀ ⦃x₁ : α⦄, x₁ s∀ ⦃x₂ : α⦄, x₂ sf x₁ = f x₂x₁ = x₂
Instances For
def Set.graphOn {α : Type u} {β : Type v} (f : αβ) (s : Set α) :
Set (α × β)

The graph of a function f : α → β on a set s.

Equations
• = (fun (x : α) => (x, f x)) '' s
Instances For
def Set.SurjOn {α : Type u} {β : Type v} (f : αβ) (s : Set α) (t : Set β) :

f is surjective from a to b if b is contained in the image of a.

Equations
Instances For
def Set.BijOn {α : Type u} {β : Type v} (f : αβ) (s : Set α) (t : Set β) :

f is bijective from s to t if f is injective on s and f '' s = t.

Equations
Instances For
def Set.LeftInvOn {α : Type u} {β : Type v} (f' : βα) (f : αβ) (s : Set α) :

g is a left inverse to f on a means that g (f x) = x for all x ∈ a.

Equations
Instances For
@[reducible, inline]
abbrev Set.RightInvOn {α : Type u} {β : Type v} (f' : βα) (f : αβ) (t : Set β) :

g is a right inverse to f on b if f (g x) = x for all x ∈ b.

Equations
Instances For
def Set.InvOn {α : Type u} {β : Type v} (g : βα) (f : αβ) (s : Set α) (t : Set β) :

g is an inverse to f viewed as a map from a to b

Equations
Instances For
def Set.image2 {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (s : Set α) (t : Set β) :
Set γ

The image of a binary function f : α → β → γ as a function Set α → Set β → Set γ. Mathematically this should be thought of as the image of the corresponding function α × β → γ.

Equations
Instances For
@[simp]
theorem Set.mem_image2 {α : Type u} {β : Type v} {γ : Type w} {f : αβγ} {s : Set α} {t : Set β} {c : γ} :
c Set.image2 f s t ∃ (a : α), a s ∃ (b : β), b t f a b = c
theorem Set.mem_image2_of_mem {α : Type u} {β : Type v} {γ : Type w} {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (ha : a s) (hb : b t) :
f a b Set.image2 f s t
def Set.seq {α : Type u} {β : Type v} (s : Set (αβ)) (t : Set α) :
Set β

Given a set s of functions α → β and t : Set α, seq s t is the union of f '' t over all f ∈ s`.

Equations
Instances For
@[simp]
theorem Set.mem_seq_iff {α : Type u} {β : Type v} {s : Set (αβ)} {t : Set α} {b : β} :
b s.seq t ∃ (f : αβ), f s ∃ (a : α), a t f a = b
theorem Set.seq_eq_image2 {α : Type u} {β : Type v} (s : Set (αβ)) (t : Set α) :
s.seq t = Set.image2 (fun (f : αβ) (a : α) => f a) s t