doc-next-gen

Mathlib.Data.Set.Restrict

Module docstring

{"# Restrict the domain of a function to a set

Main definitions

  • Set.restrict f s : restrict the domain of f to the set s;
  • Set.codRestrict f s h : given h : ∀ x, f x ∈ s, restrict the codomain of f to the set s; ","### Restrict ","### Restriction onto preimage ","### Injectivity on a set ","### Surjectivity on a set "}
Set.restrict definition
(s : Set α) (f : ∀ a : α, π a) : ∀ a : s, π a
Full source 
/-- Restrict domain of a function `f` to a set `s`. Same as `Subtype.restrict` but this version
takes an argument `↥s` instead of `Subtype s`. -/
def restrict (s : Set α) (f : ∀ a : α, π a) : ∀ a : s, π a := fun x => f x
Restriction of a function to a set
Informal description
Given a set $s$ over a type $\alpha$ and a function $f$ defined on $\alpha$, the restriction of $f$ to $s$ is the function that maps each element $x \in s$ to $f(x)$. This is equivalent to composing $f$ with the inclusion map from $s$ to $\alpha$.
Set.restrict_def theorem
(s : Set α) : s.restrict (π := π) = fun f x ↦ f x
Full source 
theorem restrict_def (s : Set α) : s.restrict (π := π) = fun f x ↦ f x := rfl
Definition of Restriction Operation on a Set
Informal description
For any set $s$ over a type $\alpha$, the restriction operation on $s$ is defined as the function that takes a function $f$ and an element $x \in s$ and returns $f(x)$. In other words, the restriction of $f$ to $s$ is the function that evaluates $f$ at each point of $s$.
Set.restrict_eq theorem
(f : α → β) (s : Set α) : s.restrict f = f ∘ Subtype.val
Full source 
theorem restrict_eq (f : α → β) (s : Set α) : s.restrict f = f ∘ Subtype.val :=
  rfl
Restriction Equals Composition with Inclusion
Informal description
For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ is equal to the composition of $f$ with the inclusion map from $s$ to $\alpha$, i.e., $\text{restrict}_s f = f \circ \text{val}$, where $\text{val} : s \to \alpha$ is the natural inclusion.
Set.restrict_id theorem
(s : Set α) : restrict s id = Subtype.val
Full source 
@[simp] lemma restrict_id (s : Set α) : restrict s id = Subtype.val := rfl
Restriction of Identity Function Equals Inclusion Map
Informal description
For any subset $s$ of a type $\alpha$, the restriction of the identity function to $s$ is equal to the inclusion map from $s$ to $\alpha$.
Set.restrict_apply theorem
(f : (a : α) → π a) (s : Set α) (x : s) : s.restrict f x = f x
Full source 
@[simp]
theorem restrict_apply (f : (a : α) → π a) (s : Set α) (x : s) : s.restrict f x = f x :=
  rfl
Value of Restricted Function at a Point: $\text{restrict}_s f (x) = f(x)$ for $x \in s$
Informal description
For any function $f \colon \alpha \to \pi$ and any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ evaluated at an element $x \in s$ equals $f(x)$.
Set.restrict_eq_iff theorem
{f : ∀ a, π a} {s : Set α} {g : ∀ a : s, π a} : restrict s f = g ↔ ∀ (a) (ha : a ∈ s), f a = g ⟨a, ha⟩
Full source 
theorem restrict_eq_iff {f : ∀ a, π a} {s : Set α} {g : ∀ a : s, π a} :
    restrictrestrict s f = g ↔ ∀ (a) (ha : a ∈ s), f a = g ⟨a, ha⟩ :=
  funext_iff.trans Subtype.forall
Characterization of Function Restriction Equality: $\text{restrict}_s f = g \leftrightarrow \forall a \in s, f(a) = g(a)$
Informal description
For any function $f \colon \alpha \to \pi$, any subset $s \subseteq \alpha$, and any function $g \colon s \to \pi$, the restriction of $f$ to $s$ equals $g$ if and only if for every element $a \in s$ (with proof $ha$), we have $f(a) = g(\langle a, ha \rangle)$.
Set.range_restrict theorem
(f : α → β) (s : Set α) : Set.range (s.restrict f) = f '' s
Full source 
@[simp]
theorem range_restrict (f : α → β) (s : Set α) : Set.range (s.restrict f) = f '' s :=
  (range_comp _ _).trans <| congr_arg (f '' ·) Subtype.range_coe
Range of Restricted Function Equals Image of Subset
Informal description
For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the range of the restriction of $f$ to $s$ is equal to the image of $s$ under $f$, i.e., $\mathrm{range}(f|_s) = f(s)$.
Set.image_restrict theorem
(f : α → β) (s t : Set α) : s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t ∩ s)
Full source 
theorem image_restrict (f : α → β) (s t : Set α) :
    s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t ∩ s) := by
  rw [restrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]
Image of Restricted Function on Preimage Equals Image of Intersection
Informal description
For any function $f \colon \alpha \to \beta$ and subsets $s, t \subseteq \alpha$, the image of the preimage of $t$ under the inclusion map $\text{val} \colon s \to \alpha$ under the restriction $f|_s$ is equal to the image of $t \cap s$ under $f$. In symbols: $$f|_s(\text{val}^{-1}(t)) = f(t \cap s).$$
Set.restrict_dite theorem
{s : Set α} [∀ x, Decidable (x ∈ s)] (f : ∀ a ∈ s, β) (g : ∀ a ∉ s, β) : (s.restrict fun a => if h : a ∈ s then f a h else g a h) = (fun a : s => f a a.2)
Full source 
@[simp]
theorem restrict_dite {s : Set α} [∀ x, Decidable (x ∈ s)] (f : ∀ a ∈ s, β)
    (g : ∀ a ∉ s, β) :
    (s.restrict fun a => if h : a ∈ s then f a h else g a h) = (fun a : s => f a a.2) :=
  funext fun a => dif_pos a.2
Restriction of Piecewise Function to Set
Informal description
Let $s$ be a decidable subset of a type $\alpha$, and let $f$ and $g$ be functions defined on $s$ and its complement $s^c$ respectively. The restriction to $s$ of the piecewise function defined by $f$ on $s$ and $g$ on $s^c$ is equal to the function $f$ restricted to $s$.
Set.restrict_dite_compl theorem
{s : Set α} [∀ x, Decidable (x ∈ s)] (f : ∀ a ∈ s, β) (g : ∀ a ∉ s, β) : (sᶜ.restrict fun a => if h : a ∈ s then f a h else g a h) = (fun a : (sᶜ : Set α) => g a a.2)
Full source 
@[simp]
theorem restrict_dite_compl {s : Set α} [∀ x, Decidable (x ∈ s)] (f : ∀ a ∈ s, β)
    (g : ∀ a ∉ s, β) :
    (sᶜ.restrict fun a => if h : a ∈ s then f a h else g a h) = (fun a : (sᶜ : Set α) => g a a.2) :=
  funext fun a => dif_neg a.2
Restriction of Piecewise Function to Complement Set
Informal description
Let $s$ be a decidable subset of a type $\alpha$, and let $f$ and $g$ be functions defined on $s$ and its complement $s^c$ respectively. Then the restriction to $s^c$ of the piecewise function defined by $f$ on $s$ and $g$ on $s^c$ is equal to the function $g$ restricted to $s^c$.
Set.restrict_ite theorem
(f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] : (s.restrict fun a => if a ∈ s then f a else g a) = s.restrict f
Full source 
@[simp]
theorem restrict_ite (f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] :
    (s.restrict fun a => if a ∈ s then f a else g a) = s.restrict f :=
  restrict_dite _ _
Restriction of Piecewise Function to Set Equals Restriction of First Function
Informal description
Let $f$ and $g$ be functions from a type $\alpha$ to a type $\beta$, and let $s$ be a decidable subset of $\alpha$. The restriction to $s$ of the piecewise function defined by $f$ on $s$ and $g$ on the complement of $s$ is equal to the restriction of $f$ to $s$. In other words, for all $x \in s$, we have $(\text{if } x \in s \text{ then } f(x) \text{ else } g(x)) = f(x)$.
Set.restrict_ite_compl theorem
(f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] : (sᶜ.restrict fun a => if a ∈ s then f a else g a) = sᶜ.restrict g
Full source 
@[simp]
theorem restrict_ite_compl (f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] :
    (sᶜ.restrict fun a => if a ∈ s then f a else g a) = sᶜ.restrict g :=
  restrict_dite_compl _ _
Restriction of Piecewise Function to Complement Set Equals Restriction of Second Function
Informal description
Let $s$ be a decidable subset of a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. The restriction to the complement $s^c$ of the function defined piecewise by $f$ on $s$ and $g$ on $s^c$ is equal to the restriction of $g$ to $s^c$. In other words: \[ \left. \left( \lambda a, \begin{cases} f(a) & \text{if } a \in s \\ g(a) & \text{otherwise} \end{cases} \right) \right|_{s^c} = g|_{s^c} \]
Set.restrict_piecewise theorem
(f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] : s.restrict (piecewise s f g) = s.restrict f
Full source 
@[simp]
theorem restrict_piecewise (f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] :
    s.restrict (piecewise s f g) = s.restrict f :=
  restrict_ite _ _ _
Restriction of Piecewise Function to Set Equals Restriction of First Function
Informal description
Let $f, g : \alpha \to \beta$ be functions and $s \subseteq \alpha$ be a decidable subset. The restriction of the piecewise function $\text{piecewise}\,s\,f\,g$ to $s$ is equal to the restriction of $f$ to $s$. That is, for all $x \in s$, we have: \[ (\text{piecewise}\,s\,f\,g)|_s(x) = f|_s(x). \]
Set.restrict_piecewise_compl theorem
(f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] : sᶜ.restrict (piecewise s f g) = sᶜ.restrict g
Full source 
@[simp]
theorem restrict_piecewise_compl (f g : α → β) (s : Set α) [∀ x, Decidable (x ∈ s)] :
    sᶜ.restrict (piecewise s f g) = sᶜ.restrict g :=
  restrict_ite_compl _ _ _
Restriction of Piecewise Function to Complement Equals Restriction of Second Function
Informal description
Let $s$ be a decidable subset of a type $\alpha$, and let $f, g : \alpha \to \beta$ be functions. The restriction of the piecewise function (defined as $f$ on $s$ and $g$ on its complement $s^c$) to the complement $s^c$ is equal to the restriction of $g$ to $s^c$. In other words: \[ \left. \left( \begin{cases} f(x) & \text{if } x \in s \\ g(x) & \text{otherwise} \end{cases} \right) \right|_{s^c} = g|_{s^c} \]
Set.restrict_extend_range theorem
(f : α → β) (g : α → γ) (g' : β → γ) : (range f).restrict (extend f g g') = fun x => g x.coe_prop.choose
Full source 
theorem restrict_extend_range (f : α → β) (g : α → γ) (g' : β → γ) :
    (range f).restrict (extend f g g') = fun x => g x.coe_prop.choose := by
  classical
  exact restrict_dite _ _
Restriction of Extended Function to Range Equals Original Function on Preimages
Informal description
Let $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be functions, and let $g' : \beta \to \gamma$ be an extension function. The restriction of the extended function $\text{extend}\,f\,g\,g'$ to the range of $f$ is equal to the function that maps each $x$ in the range of $f$ to $g(a)$, where $a$ is any element in $\alpha$ such that $f(a) = x$ (which exists by definition of the range). In other words, for $x \in \text{range}(f)$, we have: $$(\text{extend}\,f\,g\,g')|_{\text{range}(f)}(x) = g(a) \quad \text{where } f(a) = x.$$
Set.restrict_extend_compl_range theorem
(f : α → β) (g : α → γ) (g' : β → γ) : (range f)ᶜ.restrict (extend f g g') = g' ∘ Subtype.val
Full source 
@[simp]
theorem restrict_extend_compl_range (f : α → β) (g : α → γ) (g' : β → γ) :
    (range f)ᶜ.restrict (extend f g g') = g' ∘ Subtype.val := by
  classical
  exact restrict_dite_compl _ _
Restriction of Extended Function to Complement of Range Equals Composition
Informal description
For any functions $f : \alpha \to \beta$, $g : \alpha \to \gamma$, and $g' : \beta \to \gamma$, the restriction of the extended function $\text{extend}\,f\,g\,g'$ to the complement of the range of $f$ is equal to the composition of $g'$ with the inclusion map from $(range f)^c$ to $\beta$. In other words, for all $x \in (range f)^c$, we have $(\text{extend}\,f\,g\,g')\restriction_{(range f)^c}(x) = g'(x)$.
Set.restrict₂ definition
{s t : Set α} (hst : s ⊆ t) (f : ∀ a : t, π a) : ∀ a : s, π a
Full source 
/-- If a function `f` is restricted to a set `t`, and `s ⊆ t`, this is the restriction to `s`. -/
@[simp]
def restrict₂ {s t : Set α} (hst : s ⊆ t) (f : ∀ a : t, π a) : ∀ a : s, π a :=
  fun x => f ⟨x.1, hst x.2⟩
Restriction of a function to a subset
Informal description
Given a subset relation $s \subseteq t$ between two sets $s$ and $t$ of type $\alpha$, and a function $f$ defined on $t$, the restriction of $f$ to $s$ is the function that maps each element $x \in s$ to $f(x)$, where $x$ is considered as an element of $t$ via the subset inclusion.
Set.restrict₂_def theorem
{s t : Set α} (hst : s ⊆ t) : restrict₂ (π := π) hst = fun f x ↦ f ⟨x.1, hst x.2⟩
Full source 
theorem restrict₂_def {s t : Set α} (hst : s ⊆ t) :
    restrict₂ (π := π) hst = fun f x ↦ f ⟨x.1, hst x.2⟩ := rfl
Definition of Restriction to a Subset
Informal description
Given two sets $s$ and $t$ of type $\alpha$ such that $s \subseteq t$, the restriction of a function $f$ defined on $t$ to the subset $s$ is equal to the function that maps each element $x \in s$ to $f(x)$, where $x$ is considered as an element of $t$ via the subset inclusion. In other words, for any $x \in s$, we have $(\text{restrict}_2\, hst\, f)(x) = f(x)$.
Set.restrict₂_comp_restrict theorem
{s t : Set α} (hst : s ⊆ t) : (restrict₂ (π := π) hst) ∘ t.restrict = s.restrict
Full source 
theorem restrict₂_comp_restrict {s t : Set α} (hst : s ⊆ t) :
    (restrict₂ (π := π) hst) ∘ t.restrict = s.restrict := rfl
Composition of Restrictions Equals Direct Restriction
Informal description
For any sets $s$ and $t$ of type $\alpha$ with $s \subseteq t$, the composition of the restriction of a function from $t$ to $s$ with the restriction of a function from $\alpha$ to $t$ is equal to the restriction of the function from $\alpha$ to $s$. In other words, for any function $f$ defined on $\alpha$, we have: \[ (\text{restrict}_s^t \circ \text{restrict}_t^\alpha)(f) = \text{restrict}_s^\alpha(f). \]
Set.restrict₂_comp_restrict₂ theorem
{s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) : (restrict₂ (π := π) hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu)
Full source 
theorem restrict₂_comp_restrict₂ {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) :
    (restrict₂ (π := π) hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu) := rfl
Composition of Nested Restrictions Equals Direct Restriction
Informal description
For any sets $s, t, u$ of type $\alpha$ such that $s \subseteq t$ and $t \subseteq u$, the composition of the restriction from $t$ to $s$ with the restriction from $u$ to $t$ is equal to the restriction from $u$ to $s$. In other words: \[ (\text{restrict}_s^t \circ \text{restrict}_t^u) = \text{restrict}_s^u. \]
Set.range_extend_subset theorem
(f : α → β) (g : α → γ) (g' : β → γ) : range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ
Full source 
theorem range_extend_subset (f : α → β) (g : α → γ) (g' : β → γ) :
    rangerange (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ := by
  classical
  rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]
Range of Extended Function is Subset of Union of Ranges
Informal description
For any functions $f : \alpha \to \beta$, $g : \alpha \to \gamma$, and $g' : \beta \to \gamma$, the range of the extended function $\text{extend}\,f\,g\,g'$ is contained in the union of the range of $g$ and the image of the complement of the range of $f$ under $g'$. In other words: \[ \text{range}(\text{extend}\,f\,g\,g') \subseteq \text{range}(g) \cup g'(\text{range}(f)^c). \]
Set.range_extend theorem
{f : α → β} (hf : Injective f) (g : α → γ) (g' : β → γ) : range (extend f g g') = range g ∪ g' '' (range f)ᶜ
Full source 
theorem range_extend {f : α → β} (hf : Injective f) (g : α → γ) (g' : β → γ) :
    range (extend f g g') = rangerange g ∪ g' '' (range f)ᶜ := by
  refine (range_extend_subset _ _ _).antisymm ?_
  rintro z (⟨x, rfl⟩ | ⟨y, hy, rfl⟩)
  exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]
Range of Extended Function Equals Union of Ranges for Injective $f$
Informal description
Let $f : \alpha \to \beta$ be an injective function, $g : \alpha \to \gamma$ any function, and $g' : \beta \to \gamma$ an arbitrary function. Then the range of the extended function $\text{extend}\,f\,g\,g'$ is equal to the union of the range of $g$ and the image under $g'$ of the complement of the range of $f$. In other words: \[ \text{range}(\text{extend}\,f\,g\,g') = \text{range}(g) \cup g'(\text{range}(f)^c). \]
Set.codRestrict definition
(f : ι → α) (s : Set α) (h : ∀ x, f x ∈ s) : ι → s
Full source 
/-- Restrict codomain of a function `f` to a set `s`. Same as `Subtype.coind` but this version
has codomain `↥s` instead of `Subtype s`. -/
def codRestrict (f : ι → α) (s : Set α) (h : ∀ x, f x ∈ s) : ι → s := fun x => ⟨f x, h x⟩
Codomain restriction of a function to a set
Informal description
Given a function $f : \iota \to \alpha$ and a subset $s \subseteq \alpha$ such that $f(x) \in s$ for all $x \in \iota$, the function $\mathrm{codRestrict}\, f\, s\, h$ restricts the codomain of $f$ to $s$, yielding a function of type $\iota \to s$.
Set.val_codRestrict_apply theorem
(f : ι → α) (s : Set α) (h : ∀ x, f x ∈ s) (x : ι) : (codRestrict f s h x : α) = f x
Full source 
@[simp]
theorem val_codRestrict_apply (f : ι → α) (s : Set α) (h : ∀ x, f x ∈ s) (x : ι) :
    (codRestrict f s h x : α) = f x :=
  rfl
Codomain-Restricted Function Preserves Values Under Coercion
Informal description
For any function $f : \iota \to \alpha$, subset $s \subseteq \alpha$ with the property that $f(x) \in s$ for all $x \in \iota$, and any $x \in \iota$, the underlying value of the codomain-restricted function $\mathrm{codRestrict}\, f\, s\, h$ at $x$ equals $f(x)$. In other words, the coercion of $\mathrm{codRestrict}\, f\, s\, h\, x$ back to $\alpha$ is equal to $f(x)$.
Set.restrict_comp_codRestrict theorem
{f : ι → α} {g : α → β} {b : Set α} (h : ∀ x, f x ∈ b) : b.restrict g ∘ b.codRestrict f h = g ∘ f
Full source 
@[simp]
theorem restrict_comp_codRestrict {f : ι → α} {g : α → β} {b : Set α} (h : ∀ x, f x ∈ b) :
    b.restrict g ∘ b.codRestrict f h = g ∘ f :=
  rfl
Composition of Restricted and Codomain-Restricted Functions Equals Original Composition
Informal description
Let $f : \iota \to \alpha$ be a function, $g : \alpha \to \beta$ a function, and $b \subseteq \alpha$ a subset such that $f(x) \in b$ for all $x \in \iota$. Then the composition of the restriction of $g$ to $b$ with the codomain restriction of $f$ to $b$ equals the composition of $g$ with $f$, i.e., \[ \text{restrict}_b\, g \circ \text{codRestrict}_b\, f\, h = g \circ f. \]
Set.injective_codRestrict theorem
{f : ι → α} {s : Set α} (h : ∀ x, f x ∈ s) : Injective (codRestrict f s h) ↔ Injective f
Full source 
@[simp]
theorem injective_codRestrict {f : ι → α} {s : Set α} (h : ∀ x, f x ∈ s) :
    InjectiveInjective (codRestrict f s h) ↔ Injective f := by
  simp only [Injective, Subtype.ext_iff, val_codRestrict_apply]
Injectivity of Codomain-Restricted Function $\leftrightarrow$ Injectivity of Original Function
Informal description
Let $f : \iota \to \alpha$ be a function and $s \subseteq \alpha$ a subset such that $f(x) \in s$ for all $x \in \iota$. Then the codomain-restricted function $\mathrm{codRestrict}\, f\, s\, h$ is injective if and only if $f$ is injective.
Set.restrict_eq_restrict_iff theorem
: restrict s f₁ = restrict s f₂ ↔ EqOn f₁ f₂ s
Full source 
@[simp]
theorem restrict_eq_restrict_iff : restrictrestrict s f₁ = restrict s f₂ ↔ EqOn f₁ f₂ s :=
  restrict_eq_iff
Equality of Function Restrictions $\leftrightarrow$ Pointwise Equality on Subset
Informal description
For any two functions $f_1, f_2 \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the restrictions of $f_1$ and $f_2$ to $s$ are equal if and only if $f_1$ and $f_2$ agree on $s$, i.e., $f_1(x) = f_2(x)$ for all $x \in s$.
Set.MapsTo.restrict_commutes theorem
(f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) : Subtype.val ∘ h.restrict f s t = f ∘ Subtype.val
Full source 
theorem MapsTo.restrict_commutes (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) :
    Subtype.valSubtype.val ∘ h.restrict f s t = f ∘ Subtype.val :=
  rfl
Commutativity of Restriction with Inclusion Maps
Informal description
Let $f : \alpha \to \beta$ be a function, $s \subseteq \alpha$ and $t \subseteq \beta$ subsets, and $h : \text{MapsTo}\, f\, s\, t$ a proof that $f$ maps $s$ into $t$. Then the composition of the inclusion map $\text{Subtype.val} : s \to \alpha$ with the restricted function $h.\text{restrict}\, f\, s\, t : s \to t$ equals the composition of $f$ with the inclusion map $\text{Subtype.val} : s \to \alpha$. In other words, the following diagram commutes: $$\begin{array}{ccc} s & \xrightarrow{h.\text{restrict}\, f\, s\, t} & t \\ \downarrow{\text{Subtype.val}} & & \downarrow{\text{Subtype.val}} \\ \alpha & \xrightarrow{f} & \beta \end{array}$$
Set.MapsTo.val_restrict_apply theorem
(h : MapsTo f s t) (x : s) : (h.restrict f s t x : β) = f x
Full source 
@[simp]
theorem MapsTo.val_restrict_apply (h : MapsTo f s t) (x : s) : (h.restrict f s t x : β) = f x :=
  rfl
Value of Restricted Function Equals Original Function on Restricted Domain
Informal description
Let $f : \alpha \to \beta$ be a function, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be sets such that $f$ maps every element of $s$ into $t$ (i.e., $\forall x \in s, f(x) \in t$). Then for any $x \in s$, the value of the restricted function $h.\text{restrict}\,f\,s\,t$ at $x$ (considered as an element of $t$) equals $f(x)$. In other words, if $h : \text{MapsTo}\,f\,s\,t$ and $x \in s$, then $(h.\text{restrict}\,f\,s\,t\,x) = f(x)$.
Set.MapsTo.coe_iterate_restrict theorem
{f : α → α} (h : MapsTo f s s) (x : s) (k : ℕ) : h.restrict^[k] x = f^[k] x
Full source 
theorem MapsTo.coe_iterate_restrict {f : α → α} (h : MapsTo f s s) (x : s) (k : ℕ) :
    h.restrict^[k] x = f^[k] x := by
  induction k with
  | zero => simp
  | succ k ih => simp only [iterate_succ', comp_apply, val_restrict_apply, ih]
Iteration Commutes with Restriction: $(f|_{s \to s})^{[k]}(x) = f^{[k]}(x)$
Informal description
Let $f : \alpha \to \alpha$ be a function and $s \subseteq \alpha$ a subset such that $f$ maps $s$ into itself (i.e., $\forall x \in s, f(x) \in s$). Then for any $x \in s$ and natural number $k$, the $k$-th iterate of the restricted function $h.\text{restrict}\,f\,s\,s$ evaluated at $x$ equals the $k$-th iterate of $f$ evaluated at $x$, i.e., $$(h.\text{restrict}\,f\,s\,s)^{[k]}(x) = f^{[k]}(x).$$
Set.codRestrict_restrict theorem
(h : ∀ x : s, f x ∈ t) : codRestrict (s.restrict f) t h = MapsTo.restrict f s t fun x hx => h ⟨x, hx⟩
Full source 
/-- Restricting the domain and then the codomain is the same as `MapsTo.restrict`. -/
@[simp]
theorem codRestrict_restrict (h : ∀ x : s, f x ∈ t) :
    codRestrict (s.restrict f) t h = MapsTo.restrict f s t fun x hx => h ⟨x, hx⟩ :=
  rfl
Equality of Codomain-Restricted and Fully-Restricted Functions
Informal description
Given a function $f : \alpha \to \beta$, a subset $s \subseteq \alpha$, and a subset $t \subseteq \beta$ such that for every $x \in s$ we have $f(x) \in t$, then the codomain restriction of the domain-restricted function $f|_s$ to $t$ is equal to the restriction of $f$ viewed as a map from $s$ to $t$. In symbols: If $h : \forall x \in s, f(x) \in t$, then $$\mathrm{codRestrict}\, (f|_s)\, t\, h = \mathrm{MapsTo.restrict}\, f\, s\, t\, (\lambda x hx, h \langle x, hx \rangle)$$ where: - $f|_s$ denotes the restriction of $f$ to domain $s$ - $\mathrm{codRestrict}$ restricts the codomain to $t$ - $\mathrm{MapsTo.restrict}$ restricts both domain and codomain appropriately
Set.MapsTo.restrict_eq_codRestrict theorem
(h : MapsTo f s t) : h.restrict f s t = codRestrict (s.restrict f) t fun x => h x.2
Full source 
/-- Reverse of `Set.codRestrict_restrict`. -/
theorem MapsTo.restrict_eq_codRestrict (h : MapsTo f s t) :
    h.restrict f s t = codRestrict (s.restrict f) t fun x => h x.2 :=
  rfl
Equality of Function Restriction and Codomain Restriction: $f|_{s \to t} = \text{codRestrict}(f|_s, t)$
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$, the restriction of $f$ to a function from $s$ to $t$ is equal to the codomain restriction of the set-restricted function $f|_s$ to $t$.
Set.MapsTo.coe_restrict theorem
(h : Set.MapsTo f s t) : Subtype.val ∘ h.restrict f s t = s.restrict f
Full source 
theorem MapsTo.coe_restrict (h : Set.MapsTo f s t) :
    Subtype.valSubtype.val ∘ h.restrict f s t = s.restrict f :=
  rfl
Composition of Inclusion with Restricted Function Equals Restriction
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$, the composition of the inclusion map from $t$ to $\beta$ with the restricted function $h.\text{restrict}\,f\,s\,t$ equals the restriction of $f$ to $s$.
Set.MapsTo.range_restrict theorem
(f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) : range (h.restrict f s t) = Subtype.val ⁻¹' (f '' s)
Full source 
theorem MapsTo.range_restrict (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) :
    range (h.restrict f s t) = Subtype.valSubtype.val ⁻¹' (f '' s) :=
  Set.range_subtype_map f h
Range of Restricted Function Equals Preimage of Image
Informal description
Let $f : \alpha \to \beta$ be a function, $s \subseteq \alpha$ and $t \subseteq \beta$ be sets, and assume that $f$ maps every element of $s$ into $t$ (i.e., $\forall x \in s, f(x) \in t$). Then the range of the restricted function $f|_{s} : s \to t$ is equal to the preimage under the inclusion map of the image of $s$ under $f$, i.e., \[ \text{range}(f|_{s}) = (\text{incl})^{-1}(f(s)) \] where $\text{incl} : t \to \beta$ is the inclusion map.
Set.mapsTo_iff_exists_map_subtype theorem
: MapsTo f s t ↔ ∃ g : s → t, ∀ x : s, f x = g x
Full source 
theorem mapsTo_iff_exists_map_subtype : MapsToMapsTo f s t ↔ ∃ g : s → t, ∀ x : s, f x = g x :=
  ⟨fun h => ⟨h.restrict f s t, fun _ => rfl⟩, fun ⟨g, hg⟩ x hx => by
    rw [hg ⟨x, hx⟩]
    apply Subtype.coe_prop⟩
Characterization of MapsTo via Subtype Restriction
Informal description
For a function $f : \alpha \to \beta$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the following are equivalent: 1. $f$ maps every element of $s$ into $t$ (i.e., $\forall x \in s, f(x) \in t$). 2. There exists a function $g : s \to t$ such that for every $x \in s$, $f(x) = g(x)$.
Set.surjective_mapsTo_image_restrict theorem
(f : α → β) (s : Set α) : Surjective ((mapsTo_image f s).restrict f s (f '' s))
Full source 
theorem surjective_mapsTo_image_restrict (f : α → β) (s : Set α) :
    Surjective ((mapsTo_image f s).restrict f s (f '' s)) := fun ⟨_, x, hs, hxy⟩ =>
  ⟨⟨x, hs⟩, Subtype.ext hxy⟩
Surjectivity of Restricted Function onto its Image
Informal description
For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the restriction of $f$ to $s$ with codomain $f(s) = \{f(x) \mid x \in s\}$ is surjective. That is, the restricted function $f|_{s} \colon s \to f(s)$ satisfies that for every $y \in f(s)$, there exists an $x \in s$ such that $f(x) = y$.
Set.image_restrictPreimage theorem
: t.restrictPreimage f '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s)
Full source 
theorem image_restrictPreimage :
    t.restrictPreimage f '' (Subtype.val ⁻¹' s) = Subtype.valSubtype.val ⁻¹' (f '' s) := by
  delta Set.restrictPreimage
  rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]
Image-Preimage Identity for Restricted Functions: $(f|_t)(\uparrow^{-1}(s)) = \uparrow^{-1}(f(s))$
Informal description
For a function $f : \alpha \to \beta$ and subsets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the preimage $(\uparrow)^{-1}(s)$ under the restricted function $t.\mathrm{restrictPreimage}\, f$ equals the preimage of $f(s)$ under the inclusion map $\uparrow : t \to \beta$. In symbols: $$(t.\mathrm{restrictPreimage}\, f)\big((\uparrow)^{-1}(s)\big) = (\uparrow)^{-1}(f(s))$$ where $\uparrow$ denotes the canonical inclusion map from $t$ to $\beta$.
Set.range_restrictPreimage theorem
: range (t.restrictPreimage f) = Subtype.val ⁻¹' range f
Full source 
theorem range_restrictPreimage : range (t.restrictPreimage f) = Subtype.valSubtype.val ⁻¹' range f := by
  simp only [← image_univ, ← image_restrictPreimage, preimage_univ]
Range of Restricted Preimage Equals Preimage of Range
Informal description
For any function $f : \alpha \to \beta$ and subset $t \subseteq \beta$, the range of the restricted function $\mathrm{restrictPreimage}\ f\ t$ is equal to the preimage of the range of $f$ under the subtype inclusion map $\mathrm{Subtype.val} : t \to \beta$. In other words, \[ \mathrm{range}\ (\mathrm{restrictPreimage}\ f\ t) = \{x \in t \mid x \in \mathrm{range}\ f\}. \]
Set.restrictPreimage_mk theorem
(h : a ∈ f ⁻¹' t) : t.restrictPreimage f ⟨a, h⟩ = ⟨f a, h⟩
Full source 
@[simp]
theorem restrictPreimage_mk (h : a ∈ f ⁻¹' t) : t.restrictPreimage f ⟨a, h⟩ = ⟨f a, h⟩ := rfl
Evaluation of Restricted Function on Preimage Element
Informal description
For a function $f : \alpha \to \beta$ and a subset $t \subseteq \beta$, if $a \in f^{-1}(t)$, then the restriction of $f$ to the preimage $f^{-1}(t)$ evaluated at $\langle a, h \rangle$ (where $h$ is the proof that $a \in f^{-1}(t)$) equals $\langle f(a), h \rangle$.
Set.image_val_preimage_restrictPreimage theorem
{u : Set t} : Subtype.val '' (t.restrictPreimage f ⁻¹' u) = f ⁻¹' (Subtype.val '' u)
Full source 
theorem image_val_preimage_restrictPreimage {u : Set t} :
    Subtype.valSubtype.val '' (t.restrictPreimage f ⁻¹' u) = f ⁻¹' (Subtype.val '' u) := by
  ext
  simp
Image-Preimage Relation for Restricted Function
Informal description
Let $f : \alpha \to \beta$ be a function, $t \subseteq \beta$ a subset, and $u \subseteq t$ a subset of $t$. Then the image under the inclusion map $\text{val} : t \to \beta$ of the preimage of $u$ under the restricted function $\text{restrictPreimage}\ t\ f : f^{-1}(t) \to t$ is equal to the preimage under $f$ of the image of $u$ under $\text{val}$. In symbols: \[ \text{val} \left( (\text{restrictPreimage}\ t\ f)^{-1}(u) \right) = f^{-1}(\text{val}(u)). \]
Set.preimage_restrictPreimage theorem
{u : Set t} : t.restrictPreimage f ⁻¹' u = (fun a : f ⁻¹' t ↦ f a) ⁻¹' (Subtype.val '' u)
Full source 
theorem preimage_restrictPreimage {u : Set t} :
    t.restrictPreimage f ⁻¹' u = (fun a : f ⁻¹' t ↦ f a) ⁻¹' (Subtype.val '' u) := by
  rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage,
    preimage_image_eq _ Subtype.val_injective]
Preimage of Restricted Function Equals Composition Preimage
Informal description
For a function $f \colon \alpha \to \beta$, a subset $t \subseteq \beta$, and a subset $u \subseteq t$, the preimage of $u$ under the restricted function $\text{restrictPreimage}\ t\ f \colon f^{-1}(t) \to t$ is equal to the preimage of the image of $u$ under the inclusion map $\text{val} \colon t \to \beta$ composed with $f$. In symbols: \[ (\text{restrictPreimage}\ t\ f)^{-1}(u) = (f \circ \text{val})^{-1}(\text{val}(u)). \]
Set.restrictPreimage_injective theorem
(hf : Injective f) : Injective (t.restrictPreimage f)
Full source 
lemma restrictPreimage_injective (hf : Injective f) : Injective (t.restrictPreimage f) :=
  fun _ _ e => Subtype.coe_injective <| hf <| Subtype.mk.inj e
Injectivity of Restricted Function on Preimage
Informal description
Let $f : \alpha \to \beta$ be an injective function and let $t \subseteq \beta$. Then the restricted function $f \restriction_{f^{-1}(t)} : f^{-1}(t) \to t$ is also injective.
Set.restrictPreimage_surjective theorem
(hf : Surjective f) : Surjective (t.restrictPreimage f)
Full source 
lemma restrictPreimage_surjective (hf : Surjective f) : Surjective (t.restrictPreimage f) :=
  fun x => ⟨⟨_, ((hf x).choose_spec.symm ▸ x.2 : _ ∈ t)⟩, Subtype.ext (hf x).choose_spec⟩
Surjectivity of Restricted Function to Preimage
Informal description
If a function $f : \alpha \to \beta$ is surjective, then for any subset $t \subseteq \beta$, the restriction of $f$ to its preimage $f^{-1}(t)$ is a surjective function from $f^{-1}(t)$ to $t$.
Set.restrictPreimage_bijective theorem
(hf : Bijective f) : Bijective (t.restrictPreimage f)
Full source 
lemma restrictPreimage_bijective (hf : Bijective f) : Bijective (t.restrictPreimage f) :=
  ⟨t.restrictPreimage_injective hf.1, t.restrictPreimage_surjective hf.2⟩
Bijectivity of Restricted Function to Preimage
Informal description
Let $f : \alpha \to \beta$ be a bijective function and let $t \subseteq \beta$. Then the restriction of $f$ to its preimage $f^{-1}(t)$, denoted by $f \restriction_{f^{-1}(t)} : f^{-1}(t) \to t$, is also bijective.
Set.injOn_iff_injective theorem
: InjOn f s ↔ Injective (s.restrict f)
Full source 
theorem injOn_iff_injective : InjOnInjOn f s ↔ Injective (s.restrict f) :=
  ⟨fun H a b h => Subtype.eq <| H a.2 b.2 h, fun H a as b bs h =>
    congr_arg Subtype.val <| @H ⟨a, as⟩ ⟨b, bs⟩ h⟩
Injectivity on a Set is Equivalent to Injectivity of its Restriction
Informal description
A function $f : \alpha \to \beta$ is injective on a set $s \subseteq \alpha$ if and only if the restriction of $f$ to $s$, denoted by $f|_s$, is injective.
Set.MapsTo.restrict_inj theorem
(h : MapsTo f s t) : Injective (h.restrict f s t) ↔ InjOn f s
Full source 
theorem MapsTo.restrict_inj (h : MapsTo f s t) : InjectiveInjective (h.restrict f s t) ↔ InjOn f s := by
  rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]
Injectivity of Restricted Function $\leftrightarrow$ Injectivity on Domain Set
Informal description
Let $f : \alpha \to \beta$ be a function and $s \subseteq \alpha$, $t \subseteq \beta$ be sets such that $f$ maps every element of $s$ into $t$ (i.e., $f(s) \subseteq t$). Then the restriction of $f$ to a function from $s$ to $t$ is injective if and only if $f$ is injective on $s$.
Set.surjOn_iff_surjective theorem
: SurjOn f s univ ↔ Surjective (s.restrict f)
Full source 
theorem surjOn_iff_surjective : SurjOnSurjOn f s univ ↔ Surjective (s.restrict f) :=
  ⟨fun H b =>
    let ⟨a, as, e⟩ := @H b trivial
    ⟨⟨a, as⟩, e⟩,
    fun H b _ =>
    let ⟨⟨a, as⟩, e⟩ := H b
    ⟨a, as, e⟩⟩
Surjectivity of Restriction to Universal Set $\leftrightarrow$ Surjectivity of Restricted Function
Informal description
A function $f : \alpha \to \beta$ is surjective from a set $s \subseteq \alpha$ to the universal set $\text{univ} = \beta$ if and only if the restriction of $f$ to $s$, denoted by $f|_s$, is surjective.
Set.MapsTo.restrict_surjective_iff theorem
(h : MapsTo f s t) : Surjective (MapsTo.restrict _ _ _ h) ↔ SurjOn f s t
Full source 
@[simp]
theorem MapsTo.restrict_surjective_iff (h : MapsTo f s t) :
    SurjectiveSurjective (MapsTo.restrict _ _ _ h) ↔ SurjOn f s t := by
  refine ⟨fun h' b hb ↦ ?_, fun h' ⟨b, hb⟩ ↦ ?_⟩
  · obtain ⟨⟨a, ha⟩, ha'⟩ := h' ⟨b, hb⟩
    replace ha' : f a = b := by simpa [Subtype.ext_iff] using ha'
    rw [← ha']
    exact mem_image_of_mem f ha
  · obtain ⟨a, ha, rfl⟩ := h' hb
    exact ⟨⟨a, ha⟩, rfl⟩
Surjectivity of Restricted Function $\leftrightarrow$ Surjectivity on Domain and Codomain Sets
Informal description
Let $f : \alpha \to \beta$ be a function and $s \subseteq \alpha$, $t \subseteq \beta$ be sets such that $f$ maps every element of $s$ into $t$ (i.e., $f(s) \subseteq t$). Then the restriction of $f$ to a function from $s$ to $t$ is surjective if and only if $f$ is surjective from $s$ to $t$ (i.e., every element of $t$ is the image of some element in $s$).