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

source

theorem Set.ext_iff {α : Type u} {a : Set α} {b : Set α} :

a = b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b

source

@[simp]

theorem Set.mem_setOf_eq {α : Type u} {x : α} {p : α → Prop} :

(x ∈ {y : α | p y}) = p x

source

@[simp]

theorem Set.mem_univ {α : Type u} (x : α) :

x ∈ Set.univ

source

instance Set.instHasCompl {α : Type u} :

HasCompl (Set α)

Equations

Set.instHasCompl = { compl := fun (s : Set α) => {x : α | ¬x ∈ s} }

source

@[simp]

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

x ∈ sᶜ ↔ ¬x ∈ s

source

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

s \ t = s ∩ tᶜ

source

@[simp]

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

x ∈ s \ t ↔ x ∈ s ∧ ¬x ∈ t

source

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

x ∈ s \ t

source

@[reducible]

def Set.Elem {α : Type u} (s : Set α) :

Type u

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

Equations

↑s = { x : α // x ∈ s }

Instances For

source

instance Set.instCoeSortType {α : Type u} :

CoeSort (Set α) (Type u)

Coercion from a set to the corresponding subtype.

Equations

Set.instCoeSortType = { coe := Set.Elem }

source

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

f ⁻¹' s = {x : α | f x ∈ s}

source

def Set.«term_⁻¹'_» :

Lean.TrailingParserDescr

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

Equations

Set.«term_⁻¹'_» = Lean.ParserDescr.trailingNode `Set.term_⁻¹'_ 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁻¹' ") (Lean.ParserDescr.cat `term 81))

source

@[simp]

theorem Set.mem_preimage {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α} :

a ∈ f ⁻¹' s ↔ f a ∈ s

source

def Set.term_''_ :

Lean.TrailingParserDescr

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

Equations

Set.term_''_ = Lean.ParserDescr.trailingNode `Set.term_''_ 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " '' ") (Lean.ParserDescr.cat `term 81))

source

@[simp]

theorem Set.mem_image {α : Type u} {β : Type v} (f : α → β) (s : Set α) (y : β) :

y ∈ f '' s ↔ ∃ (x : α), x ∈ s ∧ f x = y

source

theorem Set.mem_image_of_mem {α : Type u} {β : Type v} (f : α → β) {x : α} {a : Set α} (h : x ∈ a) :

f x ∈ f '' a

source

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

Set.imageFactorization f s p = ⟨f ↑p, ⋯⟩

source

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

Set.kernImage f s = {y : β | ∀ ⦃x : α⦄, f x = y → x ∈ s}

source

theorem Set.subset_kernImage_iff {α : Type u} {β : Type v} {s : Set β} {t : Set α} {f : α → β} :

s ⊆ Set.kernImage f t ↔ f ⁻¹' s ⊆ t

source

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

Set.range f = {x : α | ∃ (y : ι), f y = x}

source

@[simp]

theorem Set.mem_range {α : Type u} {ι : Sort u_1} {f : ι → α} {x : α} :

x ∈ Set.range f ↔ ∃ (y : ι), f y = x

source

theorem Set.mem_range_self {α : Type u} {ι : Sort u_1} {f : ι → α} (i : ι) :

f i ∈ Set.range f

source

def Set.rangeFactorization {α : Type u} {ι : Sort u_1} (f : ι → α) :

ι → ↑(Set.range f)

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

Equations

Set.rangeFactorization f i = ⟨f i, ⋯⟩

source

noncomputable def Set.rangeSplitting {α : Type u} {β : Type v} (f : α → β) :

↑(Set.range f) → α

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

Equations

Set.rangeSplitting f x = Exists.choose ⋯

source

theorem Set.apply_rangeSplitting {α : Type u} {β : Type v} (f : α → β) (x : ↑(Set.range f)) :

f (Set.rangeSplitting f x) = ↑x

source

@[simp]

theorem Set.comp_rangeSplitting {α : Type u} {β : Type v} (f : α → β) :

f ∘ Set.rangeSplitting f = Subtype.val

source

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

s.prod t = {p : α × β | p.fst ∈ s ∧ p.snd ∈ t}

source

@[defaultInstance 1000]

instance Set.instSProd {α : Type u} {β : Type v} :

SProd (Set α) (Set β) (Set (α × β))

Equations

Set.instSProd = { sprod := Set.prod }

source

theorem Set.prod_eq {α : Type u} {β : Type v} (s : Set α) (t : Set β) :

s ×ˢ t = Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t

source

theorem Set.mem_prod_eq {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β} :

(p ∈ s ×ˢ t) = (p.fst ∈ s ∧ p.snd ∈ t)

source

@[simp]

theorem Set.mem_prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β} :

p ∈ s ×ˢ t ↔ p.fst ∈ s ∧ p.snd ∈ t

source

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)

source

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

source

def Set.diagonal (α : Type u_1) :

Set (α × α)

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

Equations

Set.diagonal α = {p : α × α | p.fst = p.snd}

source

theorem Set.mem_diagonal {α : Type u} (x : α) :

(x, x) ∈ Set.diagonal α

source

@[simp]

theorem Set.mem_diagonal_iff {α : Type u} {x : α × α} :

x ∈ Set.diagonal α ↔ x.fst = x.snd

source

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

s.offDiag = {x : α × α | x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd}

source

@[simp]

theorem Set.mem_offDiag {α : Type u} {x : α × α} {s : Set α} :

x ∈ s.offDiag ↔ x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd

source

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 ∈ s → f i ∈ t i}

source

@[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 ∈ s → f i ∈ t i

source

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

source

def Set.EqOn {α : Type u} {β : Type v} (f₁ : α → β) (f₂ : α → β) (s : Set α) :

Prop

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 ∈ s → f₁ x = f₂ x

source

def Set.MapsTo {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β) :

Prop

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

Equations

Set.MapsTo f s t = ∀ ⦃x : α⦄, x ∈ s → f x ∈ t

source

theorem Set.mapsTo_image {α : Type u} {β : Type v} (f : α → β) (s : Set α) :

Set.MapsTo f s (f '' s)

source

theorem Set.mapsTo_preimage {α : Type u} {β : Type v} (f : α → β) (t : Set β) :

Set.MapsTo f (f ⁻¹' t) t

source

def Set.MapsTo.restrict {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) :

↑s → ↑t

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

Set.MapsTo.restrict f s t h = Subtype.map f h

source

@[simp]

theorem Set.restrictPreimage_coe {α : Type u} {β : Type v} (t : Set β) (f : α → β) :

∀ (a : ↑(f ⁻¹' t)), ↑(t.restrictPreimage f a) = f ↑a

source

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

t.restrictPreimage f = Set.MapsTo.restrict f (f ⁻¹' t) t ⋯

source

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

Prop

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

Equations

Set.InjOn f s = ∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂

source

def Set.graphOn {α : Type u} {β : Type v} (f : α → β) (s : Set α) :

Set (α × β)

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

Equations

Set.graphOn f s = (fun (x : α) => (x, f x)) '' s

source

def Set.SurjOn {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β) :

Prop

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

Equations

Set.SurjOn f s t = (t ⊆ f '' s)

source

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

Prop

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

Equations

Set.BijOn f s t = (Set.MapsTo f s t ∧ Set.InjOn f s ∧ Set.SurjOn f s t)

source

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

Prop

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

Equations

Set.LeftInvOn f' f s = ∀ ⦃x : α⦄, x ∈ s → f' (f x) = x

source

@[reducible, inline]

abbrev Set.RightInvOn {α : Type u} {β : Type v} (f' : β → α) (f : α → β) (t : Set β) :

Prop

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

Equations

Set.RightInvOn f' f t = Set.LeftInvOn f f' t

source

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

Prop

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

Equations

Set.InvOn g f s t = (Set.LeftInvOn g f s ∧ Set.RightInvOn g f t)

source

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

Set.image2 f s t = {c : γ | ∃ (a : α), a ∈ s ∧ ∃ (b : β), b ∈ t ∧ f a b = c}

source

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

source

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

source