doc-next-gen

Mathlib.Topology.Hom.ContinuousEvalConst

Module docstring

{"# Bundled morphisms with continuous evaluation at a point

In this file we define a typeclass saying that F is a type of bundled morphisms (in the sense of DFunLike) with a topology on F such that evaluation at a point is continuous in f : F.

Implementation Notes

For now, we define the typeclass for non-dependent bundled functions only. Whenever we add a type of bundled dependent functions with a topology having this property, we may decide to generalize from FunLike to DFunLike. "}

ContinuousEvalConst structure
(F : Type*) (α X : outParam Type*) [FunLike F α X] [TopologicalSpace F] [TopologicalSpace X]
Full source 
/-- A typeclass saying that `F` is a type of bundled morphisms (in the sense of `DFunLike`)
with a topology on `F` such that evaluation at a point is continuous in `f : F`. -/
class ContinuousEvalConst (F : Type*) (α X : outParam Type*) [FunLike F α X]
    [TopologicalSpace F] [TopologicalSpace X] : Prop where
  continuous_eval_const (x : α) : Continuous fun f : F ↦ f x
Continuous Evaluation at a Point for Bundled Morphisms
Informal description
The structure `ContinuousEvalConst` is a typeclass that asserts a type `F` represents a collection of bundled morphisms (in the sense of `FunLike`) from `α` to `X`, where both `F` and `X` are equipped with topological spaces, and the evaluation map at any point `x : α` is continuous in `f : F`. In other words, for any fixed `x : α`, the function `F → X` given by `f ↦ f x` is continuous.
Continuous.eval_const theorem
(hf : Continuous f) (x : α) : Continuous (f · x)
Full source 
@[continuity, fun_prop]
protected theorem Continuous.eval_const (hf : Continuous f) (x : α) : Continuous (f · x) :=
  (continuous_eval_const x).comp hf
Continuity of Point Evaluation for Continuous Bundled Morphisms
Informal description
Let $f : F$ be a continuous function between topological spaces, where $F$ is a type of bundled morphisms from $\alpha$ to $X$ with continuous evaluation at any point. Then for any fixed $x \in \alpha$, the evaluation map $f \mapsto f(x)$ is continuous.
continuous_coeFun theorem
: Continuous (DFunLike.coe : F → α → X)
Full source 
theorem continuous_coeFun : Continuous (DFunLike.coe : F → α → X) :=
  continuous_pi continuous_eval_const
Continuity of the Coercion from Bundled Morphisms to Functions
Informal description
For a type $F$ of bundled morphisms from $\alpha$ to $X$ (in the sense of `FunLike`), where both $F$ and $X$ are equipped with topological spaces, the coercion function from $F$ to the function space $\alpha \to X$ is continuous.
Continuous.coeFun theorem
(hf : Continuous f) : Continuous fun z ↦ ⇑(f z)
Full source 
protected theorem Continuous.coeFun (hf : Continuous f) : Continuous fun z ↦ ⇑(f z) :=
  continuous_pi hf.eval_const
Continuity of the Coercion from Continuous Bundled Morphisms to Functions
Informal description
Let $F$ be a type of bundled morphisms from $\alpha$ to $X$ (in the sense of `FunLike`) with a topology on $F$ such that evaluation at any point is continuous. If $f : F$ is continuous, then the function $z \mapsto f(z)$ (viewed as a function from $\alpha$ to $X$) is continuous.
Filter.Tendsto.eval_const theorem
{ι : Type*} {l : Filter ι} {f : ι → F} {g : F} (hf : Tendsto f l (𝓝 g)) (a : α) : Tendsto (f · a) l (𝓝 (g a))
Full source 
protected theorem Filter.Tendsto.eval_const {ι : Type*} {l : Filter ι} {f : ι → F} {g : F}
    (hf : Tendsto f l (𝓝 g)) (a : α) : Tendsto (f · a) l (𝓝 (g a)) :=
  ((continuous_id.eval_const a).tendsto _).comp hf
Convergence of Point Evaluations for Bundled Morphisms
Informal description
Let $\iota$ be a type, $l$ a filter on $\iota$, and $f : \iota \to F$ a family of bundled morphisms converging to $g : F$ in the topology on $F$. Then for any fixed point $a \in \alpha$, the evaluation map $i \mapsto f(i)(a)$ converges to $g(a)$ in the topology on $X$.
Filter.Tendsto.coeFun theorem
{ι : Type*} {l : Filter ι} {f : ι → F} {g : F} (hf : Tendsto f l (𝓝 g)) : Tendsto (fun i ↦ ⇑(f i)) l (𝓝 ⇑g)
Full source 
protected theorem Filter.Tendsto.coeFun {ι : Type*} {l : Filter ι} {f : ι → F} {g : F}
    (hf : Tendsto f l (𝓝 g)) : Tendsto (fun i ↦ ⇑(f i)) l (𝓝 ⇑g) :=
  (continuous_id.coeFun.tendsto _).comp hf
Convergence of Bundled Morphisms Implies Convergence of Their Evaluations
Informal description
Let $\iota$ be a type, $l$ a filter on $\iota$, and $f : \iota \to F$ a family of bundled morphisms converging to $g : F$ in the topology on $F$. Then the function $i \mapsto f(i)$ (viewed as a function from $\alpha$ to $X$) converges to $g$ in the topology of continuous functions.
ContinuousAt.eval_const theorem
(hf : ContinuousAt f z) (x : α) : ContinuousAt (f · x) z
Full source 
protected nonrec theorem ContinuousAt.eval_const (hf : ContinuousAt f z) (x : α) :
    ContinuousAt (f · x) z :=
  hf.eval_const x
Continuity of Point Evaluation under Continuous Morphisms
Informal description
Let $F$ be a type of bundled morphisms from $\alpha$ to $X$ (in the sense of `FunLike`), equipped with a topology such that evaluation at any point is continuous. If $f : F$ is continuous at $z$, then for any fixed $x \in \alpha$, the evaluation map $f \mapsto f(x)$ is continuous at $z$.
ContinuousAt.coeFun theorem
(hf : ContinuousAt f z) : ContinuousAt (fun z ↦ ⇑(f z)) z
Full source 
protected nonrec theorem ContinuousAt.coeFun (hf : ContinuousAt f z) :
    ContinuousAt (fun z ↦ ⇑(f z)) z :=
  hf.coeFun
Continuity of Evaluation for Bundled Morphisms at a Point
Informal description
Let $F$ be a type of bundled morphisms from $\alpha$ to $X$ (in the sense of `FunLike`), equipped with a topology on $F$ and $X$. If $f : F$ is continuous at $z$, then the evaluation map $f \mapsto f(z)$ is also continuous at $z$.
ContinuousWithinAt.eval_const theorem
(hf : ContinuousWithinAt f s z) (x : α) : ContinuousWithinAt (f · x) s z
Full source 
protected nonrec theorem ContinuousWithinAt.eval_const (hf : ContinuousWithinAt f s z) (x : α) :
    ContinuousWithinAt (f · x) s z :=
  hf.eval_const x
Continuity of Point Evaluation within a Set for Bundled Morphisms
Informal description
Let $F$ be a type of bundled morphisms from $\alpha$ to $X$ (in the sense of `FunLike`), equipped with a topology on $F$ and $X$. If $f : F$ is continuous within a set $s$ at a point $z$, then for any fixed $x \in \alpha$, the evaluation map $f \mapsto f(x)$ is also continuous within $s$ at $z$.
ContinuousWithinAt.coeFun theorem
(hf : ContinuousWithinAt f s z) : ContinuousWithinAt (fun z ↦ ⇑(f z)) s z
Full source 
protected nonrec theorem ContinuousWithinAt.coeFun (hf : ContinuousWithinAt f s z) :
    ContinuousWithinAt (fun z ↦ ⇑(f z)) s z :=
  hf.coeFun
Continuity of Bundled Morphism Evaluation within a Set at a Point
Informal description
Let $F$ be a type of bundled morphisms from $\alpha$ to $X$ (in the sense of `FunLike`), equipped with topologies on $F$ and $X$. If $f : F$ is continuous within a set $s$ at a point $z$, then the function $z \mapsto f(z)$ (viewed as a function from $\alpha$ to $X$) is also continuous within $s$ at $z$.
ContinuousOn.eval_const theorem
(hf : ContinuousOn f s) (x : α) : ContinuousOn (f · x) s
Full source 
protected theorem ContinuousOn.eval_const (hf : ContinuousOn f s) (x : α) :
    ContinuousOn (f · x) s :=
  fun z hz ↦ (hf z hz).eval_const x
Continuity of Point Evaluation on a Set for Bundled Morphisms
Informal description
Let $F$ be a type of bundled morphisms from $\alpha$ to $X$ (in the sense of `FunLike`), equipped with topologies on $F$ and $X$. If $f : F$ is continuous on a set $s$, then for any fixed $x \in \alpha$, the evaluation map $f \mapsto f(x)$ is also continuous on $s$.
ContinuousOn.coeFun theorem
(hf : ContinuousOn f s) (x : α) : ContinuousOn (f · x) s
Full source 
protected theorem ContinuousOn.coeFun (hf : ContinuousOn f s) (x : α) : ContinuousOn (f · x) s :=
  fun z hz ↦ (hf z hz).eval_const x
Continuity of Point Evaluation on a Set for Bundled Morphisms
Informal description
Let $F$ be a type of bundled morphisms from $\alpha$ to $X$ (in the sense of `FunLike`), equipped with topologies on $F$ and $X$. If $f : F$ is continuous on a set $s$, then for any fixed $x \in \alpha$, the evaluation map $f \mapsto f(x)$ is also continuous on $s$.