Mathlib.Data.Set.Operations

Module docstring

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

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

Set.mem_setOf_eq theorem

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

Full source

@[simp, mfld_simps] theorem mem_setOf_eq {x : α} {p : α → Prop} : (x ∈ {y | p y}) = p x := rfl

Membership in Set Comprehension

Informal description

For any element $x$ of type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$, the statement $x \in \{y \mid p y\}$ is equivalent to $p x$.

Set.mem_univ theorem

(x : α) : x ∈ @univ α

Full source

@[simp, mfld_simps] theorem mem_univ (x : α) : x ∈ @univ α := trivial

Universal Set Membership: $x \in \text{univ}$ for all $x$

Informal description

For any element $x$ of type $\alpha$, $x$ belongs to the universal set $\text{univ}$ of $\alpha$.

Set.instHasCompl instance

: HasCompl (Set α)

Full source

instance : HasCompl (Set α) := ⟨fun s ↦ {x | x ∉ s}⟩

Complement Operation on Sets

Informal description

For any type $\alpha$, the set of elements of $\alpha$ has a complement operation $s \mapsto s^c$ where $s^c$ is the set of all elements of $\alpha$ not in $s$.

Set.mem_compl_iff theorem

(s : Set α) (x : α) : x ∈ sᶜ ↔ x ∉ s

Full source

@[simp] theorem mem_compl_iff (s : Set α) (x : α) : x ∈ sᶜx ∈ sᶜ ↔ x ∉ s := Iff.rfl

Characterization of Set Complement Membership

Informal description

For any set $s$ in a type $\alpha$ and any element $x \in \alpha$, $x$ belongs to the complement of $s$ if and only if $x$ does not belong to $s$. In symbols: \[ x \in s^c \leftrightarrow x \notin s. \]

Set.diff_eq theorem

(s t : Set α) : s \ t = s ∩ tᶜ

Full source

theorem diff_eq (s t : Set α) : s \ t = s ∩ tᶜ := rfl

Set Difference as Intersection with Complement

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the set difference $s \setminus t$ is equal to the intersection of $s$ with the complement of $t$, i.e., \[ s \setminus t = s \cap t^c. \]

Set.mem_diff theorem

{s t : Set α} (x : α) : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t

Full source

@[simp] theorem mem_diff {s t : Set α} (x : α) : x ∈ s \ tx ∈ s \ t ↔ x ∈ s ∧ x ∉ t := Iff.rfl

Characterization of Set Difference Membership

Informal description

For any sets $s$ and $t$ in a type $\alpha$ and any element $x \in \alpha$, $x$ belongs to the set difference $s \setminus t$ if and only if $x$ belongs to $s$ and $x$ does not belong to $t$. In symbols: \[ x \in s \setminus t \leftrightarrow x \in s \land x \notin t. \]

Set.mem_diff_of_mem theorem

{s t : Set α} {x : α} (h1 : x ∈ s) (h2 : x ∉ t) : x ∈ s \ t

Full source

theorem mem_diff_of_mem {s t : Set α} {x : α} (h1 : x ∈ s) (h2 : x ∉ t) : x ∈ s \ t := ⟨h1, h2⟩

Membership in Set Difference from Membership and Non-Membership

Informal description

For any sets $s$ and $t$ in a type $\alpha$, and any element $x \in \alpha$, if $x$ belongs to $s$ and $x$ does not belong to $t$, then $x$ belongs to the set difference $s \setminus t$.

Set.preimage definition

(f : α → β) (s : Set β) : Set α

Full source

/-- The preimage of `s : Set β` by `f : α → β`, written `f ⁻¹' s`,
  is the set of `x : α` such that `f x ∈ s`. -/
def preimage (f : α → β) (s : Set β) : Set α := {x | f x ∈ s}

Preimage of a set under a function

Informal description

Given a function $ f : \alpha \to \beta $ and a subset $ s \subseteq \beta $, the preimage $ f^{-1}(s) $ is the subset of $ \alpha $ consisting of all elements $ x $ such that $ f(x) \in s $.

Set.term_⁻¹'_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `f ⁻¹' t` denotes the preimage of `t : Set β` under the function `f : α → β`. -/
infixl:80 " ⁻¹' " => preimage

Preimage of a set under a function

Informal description

Given a function $ f : \alpha \to \beta $ and a subset $ t \subseteq \beta $, the notation $ f^{-1}(t) $ denotes the preimage of $ t $ under $ f $, which is the subset of $ \alpha $ consisting of all elements $ x $ such that $ f(x) \in t $.

Set.mem_preimage theorem

{f : α → β} {s : Set β} {a : α} : a ∈ f ⁻¹' s ↔ f a ∈ s

Full source

@[simp, mfld_simps]
theorem mem_preimage {f : α → β} {s : Set β} {a : α} : a ∈ f ⁻¹' sa ∈ f ⁻¹' s ↔ f a ∈ s := Iff.rfl

Characterization of Preimage Membership: $a \in f^{-1}(s) \leftrightarrow f(a) \in s$

Informal description

For any function $f \colon \alpha \to \beta$, set $s \subseteq \beta$, and element $a \in \alpha$, we have $a \in f^{-1}(s)$ if and only if $f(a) \in s$.

Set.term_''_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `f '' s` denotes the image of `s : Set α` under the function `f : α → β`. -/
infixl:80 " '' " => image

Image of a set under a function

Informal description

The notation $f '' s$ denotes the image of the set $s \subseteq \alpha$ under the function $f : \alpha \to \beta$, defined as $\{f(x) \mid x \in s\}$.

Set.mem_image theorem

(f : α → β) (s : Set α) (y : β) : y ∈ f '' s ↔ ∃ x ∈ s, f x = y

Full source

@[simp]
theorem mem_image (f : α → β) (s : Set α) (y : β) : y ∈ f '' sy ∈ f '' s ↔ ∃ x ∈ s, f x = y :=
  Iff.rfl

Characterization of Image Membership: $y \in f(s) \leftrightarrow \exists x \in s, f(x) = y$

Informal description

For any function $f : \alpha \to \beta$, set $s \subseteq \alpha$, and element $y \in \beta$, we have $y \in f(s)$ if and only if there exists an $x \in s$ such that $f(x) = y$.

Set.mem_image_of_mem theorem

(f : α → β) {x : α} {a : Set α} (h : x ∈ a) : f x ∈ f '' a

Full source

@[mfld_simps]
theorem mem_image_of_mem (f : α → β) {x : α} {a : Set α} (h : x ∈ a) : f x ∈ f '' a :=
  ⟨_, h, rfl⟩

Image of Element in Set is in Image of Set

Informal description

For any function $f : \alpha \to \beta$, element $x \in \alpha$, and set $a \subseteq \alpha$, if $x \in a$ then $f(x) \in f(a)$.

Set.imageFactorization definition

(f : α → β) (s : Set α) : s → f '' s

Full source

/-- Restriction of `f` to `s` factors through `s.imageFactorization f : s → f '' s`. -/
def imageFactorization (f : α → β) (s : Set α) : s → f '' s := fun p =>
  ⟨f p.1, mem_image_of_mem f p.2⟩

Image factorization function

Informal description

The function `Set.imageFactorization` takes a function $f : \alpha \to \beta$ and a set $s \subseteq \alpha$, and returns a function from $s$ to the image $f(s) \subseteq \beta$, mapping each element $x \in s$ to $f(x) \in f(s)$. More precisely, for any $x \in s$, the function sends $x$ to the pair $\langle f(x), \text{mem\_image\_of\_mem } f \text{ } x.2 \rangle$, where $x.2$ is the proof that $x \in s$.

Set.kernImage definition

(f : α → β) (s : Set α) : Set β

Full source

/-- `kernImage f s` is the set of `y` such that `f ⁻¹ y ⊆ s`. -/
def kernImage (f : α → β) (s : Set α) : Set β := {y | ∀ ⦃x⦄, f x = y → x ∈ s}

Kernel image of a function with respect to a set

Informal description

For a function $f : \alpha \to \beta$ and a set $s \subseteq \alpha$, the set $\text{kernImage}(f, s)$ consists of all elements $y \in \beta$ such that the preimage $f^{-1}(\{y\})$ is contained in $s$. In other words, $y \in \text{kernImage}(f, s)$ if and only if for every $x \in \alpha$ satisfying $f(x) = y$, we have $x \in s$.

Set.subset_kernImage_iff theorem

{s : Set β} {t : Set α} {f : α → β} : s ⊆ kernImage f t ↔ f ⁻¹' s ⊆ t

Full source

lemma subset_kernImage_iff {s : Set β} {t : Set α} {f : α → β} : s ⊆ kernImage f ts ⊆ kernImage f t ↔ f ⁻¹' s ⊆ t :=
  ⟨fun h _ hx ↦ h hx rfl,
    fun h _ hx y hy ↦ h (show f y ∈ s from hy.symm ▸ hx)⟩

Characterization of Kernel Image via Preimage Inclusion

Informal description

For any function $f : \alpha \to \beta$ and subsets $s \subseteq \beta$, $t \subseteq \alpha$, the subset $s$ is contained in the kernel image of $f$ with respect to $t$ if and only if the preimage of $s$ under $f$ is contained in $t$. In other words: $$ s \subseteq \text{kernImage}(f, t) \leftrightarrow f^{-1}(s) \subseteq t. $$

Set.range definition

(f : ι → α) : Set α

Full source

/-- 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. -/
def range (f : ι → α) : Set α := {x | ∃ y, f y = x}

Range of a function

Informal description

The range of a function $f : \iota \to \alpha$ is the set $\{x \in \alpha \mid \exists y \in \iota, f(y) = x\}$ of all elements in $\alpha$ that are images of some element in $\iota$ under $f$.

Set.mem_range theorem

{x : α} : x ∈ range f ↔ ∃ y, f y = x

Full source

@[simp] theorem mem_range {x : α} : x ∈ range fx ∈ range f ↔ ∃ y, f y = x := Iff.rfl

Characterization of Range Membership: $x \in \mathrm{range}(f) \iff \exists y, f(y) = x$

Informal description

For any element $x$ of type $\alpha$, $x$ belongs to the range of a function $f : \iota \to \alpha$ if and only if there exists an element $y$ in $\iota$ such that $f(y) = x$. In other words: $$x \in \mathrm{range}(f) \iff \exists y \in \iota,\ f(y) = x.$$

Set.mem_range_self theorem

(i : ι) : f i ∈ range f

Full source

@[mfld_simps] theorem mem_range_self (i : ι) : f i ∈ range f := ⟨i, rfl⟩

Image of Element Belongs to Range of Function

Informal description

For any function $f : \iota \to \alpha$ and any element $i \in \iota$, the image $f(i)$ belongs to the range of $f$, i.e., $f(i) \in \mathrm{range}(f)$.

Set.rangeFactorization definition

(f : ι → α) : ι → range f

Full source

/-- Any map `f : ι → α` factors through a map `rangeFactorization f : ι → range f`. -/
def rangeFactorization (f : ι → α) : ι → range f := fun i => ⟨f i, mem_range_self i⟩

Range factorization of a function

Informal description

For any function $f : \iota \to \alpha$, the range factorization of $f$ is the function that maps each element $i \in \iota$ to the pair $\langle f(i), p \rangle$ where $p$ is a proof that $f(i)$ belongs to the range of $f$. In other words, it factors $f$ through its range by restricting the codomain to $\text{range}(f) \subseteq \alpha$.

Set.rangeSplitting definition

(f : α → β) : range f → α

Full source

/-- We can use the axiom of choice to pick a preimage for every element of `range f`. -/
noncomputable def rangeSplitting (f : α → β) : range f → α := fun x => x.2.choose

Preimage selection function for a function's range

Informal description

Given a function $f : \alpha \to \beta$, the function `Set.rangeSplitting f` maps each element $y$ in the range of $f$ to some preimage $x \in \alpha$ such that $f(x) = y$. This is constructed using the axiom of choice to select a preimage for each element in the range.

Set.apply_rangeSplitting theorem

(f : α → β) (x : range f) : f (rangeSplitting f x) = x

Full source

theorem apply_rangeSplitting (f : α → β) (x : range f) : f (rangeSplitting f x) = x :=
  x.2.choose_spec

Range Splitting Property: $f(\text{rangeSplitting}\, f\, x) = x$ for $x \in \text{range}\, f$

Informal description

For any function $f : \alpha \to \beta$ and any element $x$ in the range of $f$, the function value of $f$ at the preimage selected by `rangeSplitting f` equals $x$, i.e., $f(\text{rangeSplitting}\, f\, x) = x$.

Set.comp_rangeSplitting theorem

(f : α → β) : f ∘ rangeSplitting f = Subtype.val

Full source

@[simp]
theorem comp_rangeSplitting (f : α → β) : f ∘ rangeSplitting f = Subtype.val := by
  ext
  simp only [Function.comp_apply]
  apply apply_rangeSplitting

Composition of Function with Range Splitting Equals Inclusion Map

Informal description

For any function $f : \alpha \to \beta$, the composition of $f$ with its range splitting function equals the inclusion map from the range of $f$ to $\beta$, i.e., $f \circ (\text{rangeSplitting}\, f) = \text{Subtype.val}$.

Set.prod definition

(s : Set α) (t : Set β) : Set (α × β)

Full source

/-- The cartesian product `Set.prod s t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`. -/
def prod (s : Set α) (t : Set β) : Set (α × β) := {p | p.1 ∈ s ∧ p.2 ∈ t}

Cartesian product of sets

Informal description

The cartesian product of two sets $s \subseteq \alpha$ and $t \subseteq \beta$ is the set of all pairs $(a, b)$ where $a \in s$ and $b \in t$.

Set.instSProd instance

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

Full source

@[default_instance]
instance instSProd : SProd (Set α) (Set β) (Set (α × β)) where
  sprod := Set.prod

Cartesian Product of Sets as a Set Operation

Informal description

For any types $\alpha$ and $\beta$, the Cartesian product operation $\timesˢ$ on sets $s \subseteq \alpha$ and $t \subseteq \beta$ yields a set in $\alpha \times \beta$ consisting of all pairs $(a, b)$ where $a \in s$ and $b \in t$.

Set.prod_eq theorem

(s : Set α) (t : Set β) : s ×ˢ t = Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t

Full source

theorem prod_eq (s : Set α) (t : Set β) : s ×ˢ t = Prod.fstProd.fst ⁻¹' sProd.fst ⁻¹' s ∩ Prod.snd ⁻¹' t := rfl

Cartesian Product as Intersection of Preimages

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \timesˢ t$ is equal to the intersection of the preimages of $s$ under the first projection $\text{fst} : \alpha \times \beta \to \alpha$ and of $t$ under the second projection $\text{snd} : \alpha \times \beta \to \beta$. That is, $$ s \timesˢ t = \text{fst}^{-1}(s) \cap \text{snd}^{-1}(t). $$

Set.mem_prod_eq theorem

: (p ∈ s ×ˢ t) = (p.1 ∈ s ∧ p.2 ∈ t)

Full source

theorem mem_prod_eq : (p ∈ s ×ˢ t) = (p.1 ∈ sp.1 ∈ s ∧ p.2 ∈ t) := rfl

Membership Condition for Cartesian Product of Sets: $p \in s \times t \leftrightarrow p_1 \in s \land p_2 \in t$

Informal description

For any point $p = (p_1, p_2)$ in the Cartesian product $s \timesˢ t$ of sets $s \subseteq \alpha$ and $t \subseteq \beta$, the membership condition $p \in s \timesˢ t$ is equivalent to the conjunction $p_1 \in s$ and $p_2 \in t$.

Set.mem_prod theorem

: p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t

Full source

@[simp, mfld_simps]
theorem mem_prod : p ∈ s ×ˢ tp ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t := .rfl

Membership Condition for Cartesian Product: $p \in s \times t \leftrightarrow p_1 \in s \land p_2 \in t$

Informal description

For any point $p = (p_1, p_2)$ in the Cartesian product $s \times t$ of sets $s \subseteq \alpha$ and $t \subseteq \beta$, the membership condition $p \in s \times t$ holds if and only if $p_1 \in s$ and $p_2 \in t$.

Set.prodMk_mem_set_prod_eq theorem

: ((a, b) ∈ s ×ˢ t) = (a ∈ s ∧ b ∈ t)

Full source

@[mfld_simps]
theorem prodMk_mem_set_prod_eq : ((a, b)(a, b) ∈ s ×ˢ t) = (a ∈ sa ∈ s ∧ b ∈ t) :=
  rfl

Membership Condition for Cartesian Product: $(a, b) \in s \times t \leftrightarrow a \in s \land b \in t$

Informal description

For any elements $a \in \alpha$ and $b \in \beta$, and sets $s \subseteq \alpha$ and $t \subseteq \beta$, the pair $(a, b)$ belongs to the Cartesian product $s \timesˢ t$ if and only if $a \in s$ and $b \in t$. In other words, $(a, b) \in s \timesˢ t \leftrightarrow a \in s \land b \in t$.

Set.mk_mem_prod theorem

(ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t

Full source

theorem mk_mem_prod (ha : a ∈ s) (hb : b ∈ t) : (a, b)(a, b) ∈ s ×ˢ t := ⟨ha, hb⟩

Membership in Cartesian Product: $(a, b) \in s \times t$ if $a \in s$ and $b \in t$

Informal description

For any elements $a \in \alpha$ and $b \in \beta$, if $a$ belongs to a set $s \subseteq \alpha$ and $b$ belongs to a set $t \subseteq \beta$, then the pair $(a, b)$ belongs to the Cartesian product $s \times t$.

Set.diagonal definition

(α : Type*) : Set (α × α)

Full source

/-- `diagonal α` is the set of `α × α` consisting of all pairs of the form `(a, a)`. -/
def diagonal (α : Type*) : Set (α × α) := {p | p.1 = p.2}

Diagonal of a type

Informal description

The diagonal of a type $\alpha$ is the subset of $\alpha \times \alpha$ consisting of all pairs $(a, a)$ where $a \in \alpha$.

Set.mem_diagonal theorem

(x : α) : (x, x) ∈ diagonal α

Full source

theorem mem_diagonal (x : α) : (x, x)(x, x) ∈ diagonal α := rfl

Membership of Diagonal Pairs: $(x, x) \in \text{diag}(\alpha)$

Informal description

For any element $x$ of a type $\alpha$, the pair $(x, x)$ belongs to the diagonal of $\alpha \times \alpha$.

Set.mem_diagonal_iff theorem

{x : α × α} : x ∈ diagonal α ↔ x.1 = x.2

Full source

@[simp] theorem mem_diagonal_iff {x : α × α} : x ∈ diagonal αx ∈ diagonal α ↔ x.1 = x.2 := .rfl

Characterization of Diagonal Membership: $x \in \text{diag}(\alpha) \iff x_1 = x_2$

Informal description

For any pair $x = (x_1, x_2)$ in $\alpha \times \alpha$, $x$ belongs to the diagonal of $\alpha$ if and only if its components are equal, i.e., $x_1 = x_2$.

Set.offDiag definition

(s : Set α) : Set (α × α)

Full source

/-- The off-diagonal of a set `s` is the set of pairs `(a, b)` with `a, b ∈ s` and `a ≠ b`. -/
def offDiag (s : Set α) : Set (α × α) := {x | x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2}

Off-diagonal of a set

Informal description

For a set $s$ over a type $\alpha$, the off-diagonal of $s$ is the set of all pairs $(a, b) \in \alpha \times \alpha$ such that $a, b \in s$ and $a \neq b$.

Set.mem_offDiag theorem

{x : α × α} {s : Set α} : x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

Full source

@[simp]
theorem mem_offDiag {x : α × α} {s : Set α} : x ∈ s.offDiagx ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2 :=
  Iff.rfl

Characterization of Off-Diagonal Membership: $x \in \text{offDiag}(s) \iff x_1, x_2 \in s \land x_1 \neq x_2$

Informal description

For any pair $x = (x_1, x_2)$ in $\alpha \times \alpha$ and any subset $s$ of $\alpha$, the pair $x$ belongs to the off-diagonal of $s$ if and only if both components $x_1$ and $x_2$ are elements of $s$ and $x_1 \neq x_2$. In other words: $$x \in \text{offDiag}(s) \iff (x_1 \in s) \land (x_2 \in s) \land (x_1 \neq x_2).$$

Set.pi definition

(s : Set ι) (t : ∀ i, Set (α i)) : Set (∀ i, α i)

Full source

/-- 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`. -/
def pi (s : Set ι) (t : ∀ i, Set (α i)) : Set (∀ i, α i) := {f | ∀ i ∈ s, f i ∈ t i}

Indexed product of sets

Informal description

Given an index set $s \subseteq \iota$ and a family of sets $t_i \subseteq \alpha_i$ for each $i \in \iota$, the set $\prod_{i \in s} t_i$ consists of all dependent functions $f : \prod_{i \in \iota} \alpha_i$ such that for every $i \in s$, the value $f(i)$ belongs to $t_i$.

Set.mem_pi theorem

: f ∈ s.pi t ↔ ∀ i ∈ s, f i ∈ t i

Full source

@[simp] theorem mem_pi : f ∈ s.pi tf ∈ s.pi t ↔ ∀ i ∈ s, f i ∈ t i := .rfl

Membership in Indexed Product of Sets: $f \in \prod_{i \in s} t_i \iff \forall i \in s, f(i) \in t_i$

Informal description

For any function $f$ and any family of sets $t_i$ indexed by $i \in \iota$, the function $f$ belongs to the indexed product $\prod_{i \in s} t_i$ if and only if for every index $i$ in the set $s$, the value $f(i)$ is an element of $t_i$. In other words: $$f \in \prod_{i \in s} t_i \iff \forall i \in s, f(i) \in t_i.$$

Set.mem_univ_pi theorem

: f ∈ pi univ t ↔ ∀ i, f i ∈ t i

Full source

theorem mem_univ_pi : f ∈ pi univ tf ∈ pi univ t ↔ ∀ i, f i ∈ t i := by simp

Membership in Universal Product of Sets

Informal description

A function $f$ belongs to the indexed product $\prod_{i} t_i$ of sets $t_i$ over all indices $i$ if and only if for every index $i$, the value $f(i)$ is an element of $t_i$.

Set.EqOn definition

(f₁ f₂ : α → β) (s : Set α) : Prop

Full source

/-- Two functions `f₁ f₂ : α → β` are equal on `s` if `f₁ x = f₂ x` for all `x ∈ s`. -/
def EqOn (f₁ f₂ : α → β) (s : Set α) : Prop := ∀ ⦃x⦄, x ∈ s → f₁ x = f₂ x

Equality of functions on a set

Informal description

Two functions $ f_1, f_2 : \alpha \to \beta $ are said to be equal on a set $ s \subseteq \alpha $ if for every $ x \in s $, the values $ f_1(x) $ and $ f_2(x) $ are equal.

Set.MapsTo definition

(f : α → β) (s : Set α) (t : Set β) : Prop

Full source

/-- `MapsTo f s t` means that the image of `s` is contained in `t`. -/
def MapsTo (f : α → β) (s : Set α) (t : Set β) : Prop := ∀ ⦃x⦄, x ∈ s → f x ∈ t

Image of a set under a function is contained in another set

Informal description

Given a function $f : \alpha \to \beta$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the predicate $\text{MapsTo}\, f\, s\, t$ holds if for every $x \in s$, the image $f(x)$ belongs to $t$. In other words, $f$ maps every element of $s$ into $t$.

Set.mapsTo_image theorem

(f : α → β) (s : Set α) : MapsTo f s (f '' s)

Full source

theorem mapsTo_image (f : α → β) (s : Set α) : MapsTo f s (f '' s) := fun _ ↦ mem_image_of_mem f

Image of a Set under a Function Contains All Mapped Points

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the function $f$ maps every element of $s$ into its image $f(s) = \{f(x) \mid x \in s\}$.

Set.mapsTo_preimage theorem

(f : α → β) (t : Set β) : MapsTo f (f ⁻¹' t) t

Full source

theorem mapsTo_preimage (f : α → β) (t : Set β) : MapsTo f (f ⁻¹' t) t := fun _ ↦ id

Function Maps Preimage into Target Set

Informal description

For any function $f : \alpha \to \beta$ and any subset $t \subseteq \beta$, the function $f$ maps every element of the preimage $f^{-1}(t)$ into $t$.

Set.MapsTo.restrict definition

(f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) : s → t

Full source

/-- 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`. -/
def MapsTo.restrict (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) : s → t :=
  Subtype.map f h

Restriction of a function to sets with mapping property

Informal description

Given a function $f : \alpha \to \beta$ and sets $s \subseteq \alpha$, $t \subseteq \beta$ such that $f$ maps every element of $s$ into $t$, this defines the restriction of $f$ to a function from $s$ to $t$.

Set.restrictPreimage definition

(t : Set β) (f : α → β) : f ⁻¹' t → t

Full source

/-- The restriction of a function onto the preimage of a set. -/
@[simps!]
def restrictPreimage (t : Set β) (f : α → β) : f ⁻¹' t → t :=
  (Set.mapsTo_preimage f t).restrict _ _ _

Restriction of a function to its preimage

Informal description

Given a function $ f : \alpha \to \beta $ and a subset $ t \subseteq \beta $, the function `Set.restrictPreimage` restricts $ f $ to a function from the preimage $ f^{-1}(t) $ to $ t $.

Set.InjOn definition

(f : α → β) (s : Set α) : Prop

Full source

/-- `f` is injective on `s` if the restriction of `f` to `s` is injective. -/
def InjOn (f : α → β) (s : Set α) : Prop :=
  ∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂

Injectivity on a set

Informal description

A function $f : \alpha \to \beta$ is injective on a set $s \subseteq \alpha$ if for any $x_1, x_2 \in s$, $f(x_1) = f(x_2)$ implies $x_1 = x_2$.

Set.graphOn definition

(f : α → β) (s : Set α) : Set (α × β)

Full source

/-- The graph of a function `f : α → β` on a set `s`. -/
def graphOn (f : α → β) (s : Set α) : Set (α × β) := (fun x ↦ (x, f x)) '' s

Graph of a function on a set

Informal description

The graph of a function $ f : \alpha \to \beta $ on a set $ s \subseteq \alpha $ is the set of all pairs $ (x, f(x)) $ where $ x \in s $.

Set.SurjOn definition

(f : α → β) (s : Set α) (t : Set β) : Prop

Full source

/-- `f` is surjective from `s` to `t` if `t` is contained in the image of `s`. -/
def SurjOn (f : α → β) (s : Set α) (t : Set β) : Prop := t ⊆ f '' s

Surjectivity of a function on sets

Informal description

A function $ f : \alpha \to \beta $ is surjective from a set $ s \subseteq \alpha $ to a set $ t \subseteq \beta $ if every element of $ t $ is the image of some element in $ s $, i.e., $ t \subseteq f(s) $.

Set.BijOn definition

(f : α → β) (s : Set α) (t : Set β) : Prop

Full source

/-- `f` is bijective from `s` to `t` if `f` is injective on `s` and `f '' s = t`. -/
def BijOn (f : α → β) (s : Set α) (t : Set β) : Prop := MapsToMapsTo f s t ∧ InjOn f s ∧ SurjOn f s t

Bijectivity of a function on sets

Informal description

A function $ f : \alpha \to \beta $ is bijective from a set $ s \subseteq \alpha $ to a set $ t \subseteq \beta $ if $ f $ maps $ s $ into $ t $, is injective on $ s $, and is surjective from $ s $ to $ t $ (i.e., $ f(s) = t $).

Set.LeftInvOn definition

(g : β → α) (f : α → β) (s : Set α) : Prop

Full source

/-- `g` is a left inverse to `f` on `s` means that `g (f x) = x` for all `x ∈ s`. -/
def LeftInvOn (g : β → α) (f : α → β) (s : Set α) : Prop := ∀ ⦃x⦄, x ∈ s → g (f x) = x

Left inverse of a function on a set

Informal description

A function $g : \beta \to \alpha$ is called a left inverse of $f : \alpha \to \beta$ on a set $s \subseteq \alpha$ if for every $x \in s$, the composition $g(f(x))$ equals $x$.

Set.RightInvOn abbrev

(g : β → α) (f : α → β) (t : Set β) : Prop

Full source

/-- `g` is a right inverse to `f` on `t` if `f (g x) = x` for all `x ∈ t`. -/
abbrev RightInvOn (g : β → α) (f : α → β) (t : Set β) : Prop := LeftInvOn f g t

Right Inverse Condition on a Set

Informal description

A function $g : \beta \to \alpha$ is called a right inverse of $f : \alpha \to \beta$ on a set $t \subseteq \beta$ if for every $x \in t$, the composition $f(g(x))$ equals $x$.

Set.InvOn definition

(g : β → α) (f : α → β) (s : Set α) (t : Set β) : Prop

Full source

/-- `g` is an inverse to `f` viewed as a map from `s` to `t` -/
def InvOn (g : β → α) (f : α → β) (s : Set α) (t : Set β) : Prop :=
  LeftInvOnLeftInvOn g f s ∧ RightInvOn g f t

Inverse function on sets

Informal description

A function $g : \beta \to \alpha$ is called an inverse of $f : \alpha \to \beta$ on sets $s \subseteq \alpha$ and $t \subseteq \beta$ if $g$ is both a left inverse of $f$ on $s$ (i.e., $g(f(x)) = x$ for all $x \in s$) and a right inverse of $f$ on $t$ (i.e., $f(g(y)) = y$ for all $y \in t$).

Set.image2 definition

(f : α → β → γ) (s : Set α) (t : Set β) : Set γ

Full source

/-- 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 `α × β → γ`. -/
def image2 (f : α → β → γ) (s : Set α) (t : Set β) : Set γ := {c | ∃ a ∈ s, ∃ b ∈ t, f a b = c}

Image of a binary function on sets

Informal description

Given a binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image $\text{image2}(f, s, t)$ is the set $\{f(a, b) \mid a \in s, b \in t\}$ of all outputs obtained by applying $f$ to pairs $(a, b)$ where $a$ ranges over $s$ and $b$ ranges over $t$.

Set.mem_image2 theorem

: c ∈ image2 f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c

Full source

@[simp] theorem mem_image2 : c ∈ image2 f s tc ∈ image2 f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c := .rfl

Membership in Binary Image Set: $c \in \text{image2}(f, s, t) \leftrightarrow \exists a \in s, \exists b \in t, f(a, b) = c$

Informal description

An element $c$ belongs to the image $\text{image2}(f, s, t)$ of a binary function $f$ on sets $s$ and $t$ if and only if there exist elements $a \in s$ and $b \in t$ such that $f(a, b) = c$.

Set.mem_image2_of_mem theorem

(ha : a ∈ s) (hb : b ∈ t) : f a b ∈ image2 f s t

Full source

theorem mem_image2_of_mem (ha : a ∈ s) (hb : b ∈ t) : f a b ∈ image2 f s t :=
  ⟨a, ha, b, hb, rfl⟩

Membership in Binary Image Set via Elements

Informal description

For any elements $a \in s$ and $b \in t$, the value $f(a, b)$ belongs to the image $\text{image2}(f, s, t)$.

Set.seq definition

(s : Set (α → β)) (t : Set α) : Set β

Full source

/-- Given a set `s` of functions `α → β` and `t : Set α`, `seq s t` is the union of `f '' t` over
all `f ∈ s`. -/
def seq (s : Set (α → β)) (t : Set α) : Set β := image2 (fun f ↦ f) s t

Monadic sequence operation on sets

Informal description

Given a set $s$ of functions from $\alpha$ to $\beta$ and a set $t \subseteq \alpha$, the set $\text{seq}(s, t)$ is the union of the images $f(t)$ for all $f \in s$. In other words, it consists of all elements $b \in \beta$ such that there exists a function $f \in s$ and an element $a \in t$ with $f(a) = b$.

Set.mem_seq_iff theorem

{s : Set (α → β)} {t : Set α} {b : β} : b ∈ seq s t ↔ ∃ f ∈ s, ∃ a ∈ t, (f : α → β) a = b

Full source

@[simp]
theorem mem_seq_iff {s : Set (α → β)} {t : Set α} {b : β} :
    b ∈ seq s tb ∈ seq s t ↔ ∃ f ∈ s, ∃ a ∈ t, (f : α → β) a = b :=
  Iff.rfl

Characterization of Membership in Sequential Application of Sets

Informal description

For any set $s$ of functions from $\alpha$ to $\beta$, any set $t \subseteq \alpha$, and any element $b \in \beta$, the element $b$ belongs to the sequential application $\text{seq}(s, t)$ if and only if there exists a function $f \in s$ and an element $a \in t$ such that $f(a) = b$.

Set.seq_eq_image2 theorem

(s : Set (α → β)) (t : Set α) : seq s t = image2 (fun f a ↦ f a) s t

Full source

lemma seq_eq_image2 (s : Set (α → β)) (t : Set α) : seq s t = image2 (fun f a ↦ f a) s t := rfl

Equality of Sequential Application and Binary Image: $\text{seq}(s, t) = \text{image2}(\cdot, s, t)$

Informal description

For any set $s$ of functions from $\alpha$ to $\beta$ and any set $t \subseteq \alpha$, the sequential application of $s$ to $t$ is equal to the image of the binary operation $(f, a) \mapsto f(a)$ applied to $s$ and $t$. In other words, we have: $$ \text{seq}(s, t) = \{f(a) \mid f \in s, a \in t\} $$