doc-next-gen

Mathlib.Topology.ContinuousMap.Defs

Module docstring

{"# Continuous bundled maps

In this file we define the type ContinuousMap of continuous bundled maps.

We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types. ","### Continuous maps "}

ContinuousMap structure
(X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y]
Full source 
/-- The type of continuous maps from `X` to `Y`.

When possible, instead of parametrizing results over `(f : C(X, Y))`,
you should parametrize over `{F : Type*} [ContinuousMapClass F X Y] (f : F)`.

When you extend this structure, make sure to extend `ContinuousMapClass`. -/
structure ContinuousMap (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] where
  /-- The function `X → Y` -/
  protected toFun : X → Y
  /-- Proposition that `toFun` is continuous -/
  protected continuous_toFun : Continuous toFun := by continuity
Continuous Maps between Topological Spaces
Informal description
The structure representing the type of continuous maps from a topological space \( X \) to a topological space \( Y \). When possible, instead of parametrizing results over a specific continuous map \( f : C(X, Y) \), it is recommended to parametrize over a type \( F \) equipped with a `ContinuousMapClass` instance, which ensures \( F \) consists of continuous maps from \( X \) to \( Y \).
ContinuousMapClass structure
(F : Type*) (X Y : outParam Type*) [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X Y]
Full source 
/-- `ContinuousMapClass F X Y` states that `F` is a type of continuous maps.

You should extend this class when you extend `ContinuousMap`. -/
class ContinuousMapClass (F : Type*) (X Y : outParam Type*)
    [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X Y] : Prop where
  /-- Continuity -/
  map_continuous (f : F) : Continuous f
Continuous Map Class
Informal description
The class `ContinuousMapClass F X Y` states that `F` is a type of continuous maps between topological spaces `X` and `Y`, where `F` has a function-like structure (as expressed by `FunLike F X Y`). This class is used as a base for defining various types of continuous maps and should be extended when introducing new types of continuous maps.
toContinuousMap definition
(f : F) : C(X, Y)
Full source 
/-- Coerce a bundled morphism with a `ContinuousMapClass` instance to a `ContinuousMap`. -/
@[coe] def toContinuousMap (f : F) : C(X, Y) := ⟨f, map_continuous f⟩
Conversion to bundled continuous map
Informal description
Given a type `F` equipped with a `ContinuousMapClass` instance, the function `toContinuousMap` converts an element `f : F` into a bundled continuous map `C(X, Y)`, where `X` and `Y` are topological spaces. This ensures that `f` is treated as a continuous function from `X` to `Y`.
instCoeTCContinuousMap instance
: CoeTC F C(X, Y)
Full source 
instance : CoeTC F C(X, Y) := ⟨toContinuousMap⟩
Canonical Coercion to Continuous Maps
Informal description
For any type `F` equipped with a `ContinuousMapClass` instance, there is a canonical coercion from `F` to the type `C(X, Y)` of continuous maps between topological spaces `X` and `Y`.
ContinuousMap.instFunLike instance
: FunLike C(X, Y) X Y
Full source 
instance instFunLike : FunLike C(X, Y) X Y where
  coe := ContinuousMap.toFun
  coe_injective' f g h := by cases f; cases g; congr
Function-Like Structure of Continuous Maps
Informal description
The type `C(X, Y)` of continuous maps between topological spaces $X$ and $Y$ has a function-like structure, meaning that each continuous map can be treated as a function from $X$ to $Y$ with an injective coercion.
ContinuousMap.instContinuousMapClass instance
: ContinuousMapClass C(X, Y) X Y
Full source 
instance instContinuousMapClass : ContinuousMapClass C(X, Y) X Y where
  map_continuous := ContinuousMap.continuous_toFun
Continuous Maps as Continuous Map Class
Informal description
The type `C(X, Y)` of continuous maps between topological spaces $X$ and $Y$ forms a `ContinuousMapClass`, meaning it inherits the structure of continuous maps and can be treated as a collection of functions from $X$ to $Y$ that are continuous.
ContinuousMap.toFun_eq_coe theorem
{f : C(X, Y)} : f.toFun = (f : X → Y)
Full source 
@[simp]
theorem toFun_eq_coe {f : C(X, Y)} : f.toFun = (f : X → Y) :=
  rfl
Equality of Underlying Function and Coercion for Continuous Maps
Informal description
For any continuous map $f \colon X \to Y$ between topological spaces, the underlying function $f.\text{toFun}$ is equal to the coercion of $f$ to a function $X \to Y$.
ContinuousMap.instCanLiftForallCoeContinuous instance
: CanLift (X → Y) C(X, Y) DFunLike.coe Continuous
Full source 
instance : CanLift (X → Y) C(X, Y) DFunLike.coe Continuous := ⟨fun f hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩
Lifting Continuous Functions to Continuous Maps
Informal description
For any topological spaces $X$ and $Y$, there is a canonical way to lift a continuous function $f \colon X \to Y$ to an element of the type $C(X, Y)$ of continuous maps between $X$ and $Y$.
ContinuousMap.Simps.apply definition
(f : C(X, Y)) : X → Y
Full source 
/-- See note [custom simps projection]. -/
def Simps.apply (f : C(X, Y)) : X → Y := f
Underlying function of a continuous map
Informal description
The function that extracts the underlying function from a continuous map \( f \colon X \to Y \) between topological spaces.
ContinuousMap.coe_coe theorem
{F : Type*} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) : ⇑(f : C(X, Y)) = f
Full source 
@[simp]
protected theorem coe_coe {F : Type*} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) :
    ⇑(f : C(X, Y)) = f :=
  rfl
Equality of Underlying Functions in Continuous Maps
Informal description
For any type $F$ equipped with a function-like structure and a continuous map class instance from topological spaces $X$ to $Y$, and for any element $f \in F$, the underlying function of the bundled continuous map $f \colon C(X, Y)$ is equal to $f$ itself.
ContinuousMap.coe_apply theorem
{F : Type*} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) (x : X) : (f : C(X, Y)) x = f x
Full source 
protected theorem coe_apply {F : Type*} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) (x : X) :
    (f : C(X, Y)) x = f x :=
  rfl
Evaluation Consistency for Bundled Continuous Maps
Informal description
For any type $F$ equipped with a function-like structure and a continuous map class instance from topological spaces $X$ to $Y$, and for any element $f \in F$ and point $x \in X$, the evaluation of the bundled continuous map $(f : C(X, Y))$ at $x$ equals the evaluation of $f$ at $x$, i.e., $(f : C(X, Y))(x) = f(x)$.
ContinuousMap.ext theorem
{f g : C(X, Y)} (h : ∀ a, f a = g a) : f = g
Full source 
@[ext]
theorem ext {f g : C(X, Y)} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext _ _ h
Extensionality of Continuous Maps
Informal description
For any two continuous maps $f, g \colon X \to Y$ between topological spaces, if $f(a) = g(a)$ for all $a \in X$, then $f = g$.
ContinuousMap.copy definition
(f : C(X, Y)) (f' : X → Y) (h : f' = f) : C(X, Y)
Full source 
/-- Copy of a `ContinuousMap` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : C(X, Y)) (f' : X → Y) (h : f' = f) : C(X, Y) where
  toFun := f'
  continuous_toFun := h.symm ▸ f.continuous_toFun
Copy of a continuous map with a new function
Informal description
Given a continuous map \( f \colon X \to Y \) between topological spaces and a function \( f' \colon X \to Y \) that is definitionally equal to \( f \), the function `ContinuousMap.copy` constructs a new continuous map with the underlying function \( f' \), maintaining the continuity property of \( f \). This is useful for fixing definitional equalities when working with continuous maps.
ContinuousMap.coe_copy theorem
(f : C(X, Y)) (f' : X → Y) (h : f' = f) : ⇑(f.copy f' h) = f'
Full source 
@[simp]
theorem coe_copy (f : C(X, Y)) (f' : X → Y) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl
Underlying Function of Copied Continuous Map Equals Original Function
Informal description
For any continuous map $f \colon X \to Y$ between topological spaces, and any function $f' \colon X \to Y$ such that $f' = f$, the underlying function of the copied continuous map $f.copy\, f'\, h$ is equal to $f'$.
ContinuousMap.copy_eq theorem
(f : C(X, Y)) (f' : X → Y) (h : f' = f) : f.copy f' h = f
Full source 
theorem copy_eq (f : C(X, Y)) (f' : X → Y) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h
Equality of Continuous Map Copy with Original
Informal description
For any continuous map $f \colon X \to Y$ between topological spaces and any function $f' \colon X \to Y$ such that $f' = f$, the copy of $f$ with underlying function $f'$ is equal to $f$ itself.
ContinuousMap.continuous theorem
(f : C(X, Y)) : Continuous f
Full source 
/-- Deprecated. Use `map_continuous` instead. -/
protected theorem continuous (f : C(X, Y)) : Continuous f :=
  f.continuous_toFun
Continuity of Continuous Maps
Informal description
For any continuous map $f \colon X \to Y$ between topological spaces, the underlying function $f$ is continuous.
ContinuousMap.congr_fun theorem
{f g : C(X, Y)} (H : f = g) (x : X) : f x = g x
Full source 
/-- Deprecated. Use `DFunLike.congr_fun` instead. -/
protected theorem congr_fun {f g : C(X, Y)} (H : f = g) (x : X) : f x = g x :=
  H ▸ rfl
Function Application Respects Equality for Continuous Maps
Informal description
For any continuous maps $f, g \colon X \to Y$ between topological spaces, if $f = g$, then $f(x) = g(x)$ for all $x \in X$.
ContinuousMap.congr_arg theorem
(f : C(X, Y)) {x y : X} (h : x = y) : f x = f y
Full source 
/-- Deprecated. Use `DFunLike.congr_arg` instead. -/
protected theorem congr_arg (f : C(X, Y)) {x y : X} (h : x = y) : f x = f y :=
  h ▸ rfl
Function Application Respects Equality for Continuous Maps
Informal description
For any continuous map $f \colon X \to Y$ between topological spaces and any points $x, y \in X$ such that $x = y$, we have $f(x) = f(y)$.
ContinuousMap.coe_injective theorem
: Function.Injective (DFunLike.coe : C(X, Y) → (X → Y))
Full source 
theorem coe_injective : Function.Injective (DFunLike.coe : C(X, Y) → (X → Y)) :=
  DFunLike.coe_injective
Injectivity of the Continuous Map to Function Coercion
Informal description
The canonical map from the type of continuous maps $C(X, Y)$ to the type of functions $X \to Y$ is injective. That is, if two continuous maps $f, g \colon X \to Y$ satisfy $f(x) = g(x)$ for all $x \in X$, then $f = g$.
ContinuousMap.coe_mk theorem
(f : X → Y) (h : Continuous f) : ⇑(⟨f, h⟩ : C(X, Y)) = f
Full source 
@[simp]
theorem coe_mk (f : X → Y) (h : Continuous f) : ⇑(⟨f, h⟩ : C(X, Y)) = f :=
  rfl
Underlying Function of Continuous Map Construction Equals Original Function
Informal description
For any continuous function $f \colon X \to Y$ between topological spaces, the underlying function of the continuous map $\langle f, h \rangle$ (where $h$ is a proof of continuity) is equal to $f$ itself.