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

Notation

• 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

Lemmas about mem and setOf

@[simp]

theorem Set.mem_setOf_eq {α : Type u} {x : α} {p : α → Prop} : (x ∈ {y : α | p y}) = p x

theorem Set.eq_mem_setOf {α : Type u} (p : α → Prop) : p = fun (x : α) => x ∈ {a : α | p a}

This lemma is intended for use with rw where a membership predicate is needed, hence the explicit argument and the equality in the reverse direction from normal. See also Set.mem_setOf_eq for the reverse direction applied to an argument.

theorem Set.mem_setOf {α : Type u} {a : α} {p : α → Prop} : a ∈ {x : α | p x} ↔ p a

theorem Membership.mem.out {α : Type u} {a : α} {p : α → Prop} : 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.notMem_setOf_iff {α : Type u} {a : α} {p : α → Prop} : ¬a ∈ {x : α | p x} ↔ ¬p a

@[deprecated Set.notMem_setOf_iff (since := "2025-05-24")]

theorem Set.nmem_setOf_iff {α : Type u} {a : α} {p : α → Prop} : ¬a ∈ {x : α | p x} ↔ ¬p a

Alias of Set.notMem_setOf_iff.

@[simp]

theorem Set.setOf_mem_eq {α : Type u} {s : Set α} : {x : α | x ∈ s} = s

@[simp]

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

Operations

instance Set.instHasCompl {α : Type u} : HasCompl (Set α)

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

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}

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

@[simp]

theorem Set.mem_preimage {α : Type u} {β : Type v} {f : α → β} {s : Set β} {a : α} : a ∈ f ⁻¹' s ↔ f a ∈ s

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

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

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

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}

theorem Set.subset_kernImage_iff {α : Type u} {β : Type v} {s : Set β} {t : Set α} {f : α → β} : s ⊆ kernImage f t ↔ 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

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

@[simp]

theorem Set.mem_range {α : Type u} {ι : Sort u_1} {f : ι → α} {x : α} : x ∈ range f ↔ ∃ (y : ι), f y = x

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

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

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

Equations

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

@[simp]

theorem Set.rangeFactorization_injective {α : Type u} {ι : Sort u_1} {f : ι → α} : Function.Injective (rangeFactorization f) ↔ Function.Injective f

@[simp]

theorem Set.rangeFactorization_surjective {α : Type u} {ι : Sort u_1} {f : ι → α} : Function.Surjective (rangeFactorization f)

@[simp]

theorem Set.rangeFactorization_bijective {α : Type u} {ι : Sort u_1} {f : ι → α} : Function.Bijective (rangeFactorization f) ↔ Function.Injective f

noncomputable def Set.rangeSplitting {α : Type u} {β : Type v} (f : α → β) : ↑(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 ⋯

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

@[simp]

theorem Set.comp_rangeSplitting {α : Type u} {β : Type v} (f : α → β) : f ∘ rangeSplitting f = Subtype.val

theorem Set.Subtype.range_coind {α : Type u} {β : Type v} (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)) : range (Subtype.coind f h) = Subtype.val ⁻¹' range f

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}

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

theorem Set.prod_image_left {α : Type u} {β : Type v} {γ : Type w} (f : α → γ) (s : Set α) (t : Set β) : (f '' s) ×ˢ t = (fun (x : α × β) => (f x.fst, x.snd)) '' s ×ˢ t

theorem Set.prod_image_right {α : Type u} {β : Type v} {γ : Type w} (f : α → γ) (s : Set α) (t : Set β) : t ×ˢ (f '' s) = (fun (x : β × α) => (x.fst, f x.snd)) '' t ×ˢ s

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}

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

@[simp]

theorem Set.mem_diagonal_iff {α : Type u} {x : α × α} : x ∈ diagonal α ↔ 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

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

@[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 i belongs to t i whenever i ∈ s.

Equations

• s.pi t = {f : (i : ι) → α i | ∀ (i : ι), i ∈ s → f 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 ∈ s → f i ∈ t i

theorem Set.mem_univ_pi {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {f : (i : ι) → α i} : f ∈ univ.pi t ↔ ∀ (i : ι), f i ∈ t i

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

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

MapsTo f s t means that the image of s is contained in t.

Equations

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

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

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

def Set.MapsTo.restrict {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β) (h : 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

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 ⋯

@[simp]

theorem Set.restrictPreimage_coe {α : Type u} {β : Type v} (t : Set β) (f : α → β) (a✝ : ↑(f ⁻¹' t)) : ↑(t.restrictPreimage f a✝) = f ↑a✝

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

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

Equations

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

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

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

f is surjective from s to t if t is contained in the image of s.

Equations

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

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)

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

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

Equations

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

@[reducible, inline]

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

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

Equations

• Set.RightInvOn g f t = Set.LeftInvOn f g t

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 s to t

Equations

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

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}

@[simp]

theorem Set.mem_image2 {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Set α} {t : Set β} {c : γ} : c ∈ 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 ∈ 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

• s.seq t = Set.image2 (fun (f : α → β) => f) s t

@[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 = image2 (fun (f : α → β) (a : α) => f a) s t