Mathlib.Topology.Hom.ContinuousEval

ContinuousEval structure

(F : Type*) (X Y : outParam Type*) [FunLike F X Y] [TopologicalSpace F] [TopologicalSpace X] [TopologicalSpace Y]

Full source

/-- A typeclass saying that `F` is a bundled morphism class (in the sense of `FunLike`)
with a topology such that `fun (f, x) : F × X ↦ f x` is a continuous function. -/
class ContinuousEval (F : Type*) (X Y : outParam Type*) [FunLike F X Y]
    [TopologicalSpace F] [TopologicalSpace X] [TopologicalSpace Y] : Prop where
  /-- Evaluation of a bundled morphism at a point is continuous in both variables. -/
  continuous_eval : Continuous fun fx : F × X ↦ fx.1 fx.2

Continuous Evaluation of Bundled Morphisms

Informal description

The structure `ContinuousEval F X Y` asserts that `F` is a type of bundled morphisms (in the sense of `FunLike`) from `X$ to $\Y$ with topologies on `F`, `X`, and `Y` such that the evaluation map $(f, x) \mapsto f(x)$ is continuous.

Continuous.eval theorem

(hf : Continuous f) (hg : Continuous g) : Continuous fun z ↦ f z (g z)

Full source

@[continuity, fun_prop]
protected theorem Continuous.eval (hf : Continuous f) (hg : Continuous g) :
    Continuous fun z ↦ f z (g z) :=
  continuous_eval.comp (hf.prodMk hg)

Continuity of Function Evaluation at Continuous Functions

Informal description

Let $f$ and $g$ be continuous functions. Then the function $z \mapsto f(z)(g(z))$ is continuous.

ContinuousEval.toContinuousMapClass instance

: ContinuousMapClass F X Y

Full source

instance (priority := 100) ContinuousEval.toContinuousMapClass : ContinuousMapClass F X Y where
  map_continuous _ := continuous_const.eval continuous_id

Continuous Evaluation Implies Continuous Map Class

Informal description

For any type $F$ of bundled morphisms from $X$ to $Y$ with topologies on $F$, $X$, and $Y$ such that the evaluation map $(f, x) \mapsto f(x)$ is continuous, $F$ is also a continuous map class from $X$ to $Y$.

ContinuousEval.toContinuousEvalConst instance

: ContinuousEvalConst F X Y

Full source

instance (priority := 100) ContinuousEval.toContinuousEvalConst : ContinuousEvalConst F X Y where
  continuous_eval_const _ := continuous_id.eval continuous_const

Continuous Evaluation Implies Pointwise Continuous Evaluation

Informal description

For any type `F` of bundled morphisms from `X` to `Y` with a topology such that evaluation is jointly continuous (i.e., `ContinuousEval F X Y` holds), the evaluation at any fixed point `x : X` is continuous in `f : F`. In other words, `F` satisfies `ContinuousEvalConst F X Y`.

Filter.Tendsto.eval theorem

 {α : Type*} {l : Filter α} {f : α → F} {f₀ : F} {g : α → X} {x₀ : X} (hf : Tendsto f l (𝓝 f₀))
  (hg : Tendsto g l (𝓝 x₀)) : Tendsto (fun a ↦ f a (g a)) l (𝓝 (f₀ x₀))

Full source

protected theorem Filter.Tendsto.eval {α : Type*} {l : Filter α} {f : α → F} {f₀ : F}
    {g : α → X} {x₀ : X} (hf : Tendsto f l (𝓝 f₀)) (hg : Tendsto g l (𝓝 x₀)) :
    Tendsto (fun a ↦ f a (g a)) l (𝓝 (f₀ x₀)) :=
  (ContinuousEval.continuous_eval.tendsto _).comp (hf.prodMk_nhds hg)

Continuity of Evaluation under Filter Limits

Informal description

Let $\alpha$ be a type, $l$ a filter on $\alpha$, and $f : \alpha \to F$, $g : \alpha \to X$ functions. If $f$ tends to $f_0$ in the neighborhood filter of $f_0$ and $g$ tends to $x_0$ in the neighborhood filter of $x_0$, then the evaluation function $a \mapsto f(a)(g(a))$ tends to $f_0(x_0)$ in the neighborhood filter of $f_0(x_0)$.

ContinuousAt.eval theorem

(hf : ContinuousAt f z) (hg : ContinuousAt g z) : ContinuousAt (fun z ↦ f z (g z)) z

Full source

protected nonrec theorem ContinuousAt.eval (hf : ContinuousAt f z) (hg : ContinuousAt g z) :
    ContinuousAt (fun z ↦ f z (g z)) z :=
  hf.eval hg

Continuity of Evaluation at a Point

Informal description

Let $F$ be a type of bundled morphisms from $X$ to $Y$ with topologies on $F$, $X$, and $Y$ such that evaluation is continuous (i.e., $(f,x) \mapsto f(x)$ is continuous). If $f : Z \to F$ is continuous at $z \in Z$ and $g : Z \to X$ is continuous at $z$, then the evaluation function $z \mapsto f(z)(g(z))$ is continuous at $z$.

ContinuousWithinAt.eval theorem

(hf : ContinuousWithinAt f s z) (hg : ContinuousWithinAt g s z) : ContinuousWithinAt (fun z ↦ f z (g z)) s z

Full source

protected nonrec theorem ContinuousWithinAt.eval (hf : ContinuousWithinAt f s z)
    (hg : ContinuousWithinAt g s z) : ContinuousWithinAt (fun z ↦ f z (g z)) s z :=
  hf.eval hg

Continuity of Evaluation Within a Set at a Point

Informal description

Let $F$ be a type of bundled morphisms from $X$ to $Y$ with topologies on $F$, $X$, and $Y$ such that evaluation is continuous (i.e., $(f, x) \mapsto f(x)$ is continuous). Given functions $f : X \to F$ and $g : X \to X$ that are continuous within a set $s$ at a point $z$, the evaluation function $z \mapsto f(z)(g(z))$ is also continuous within $s$ at $z$.

ContinuousOn.eval theorem

(hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun z ↦ f z (g z)) s

Full source

protected theorem ContinuousOn.eval (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun z ↦ f z (g z)) s :=
  fun z hz ↦ (hf z hz).eval (hg z hz)

Continuity of Evaluation on a Set

Informal description

Let $F$ be a type of bundled morphisms from $X$ to $Y$ with topologies on $F$, $X$, and $Y$ such that evaluation is continuous (i.e., $(f, x) \mapsto f(x)$ is continuous). Given functions $f : Z \to F$ and $g : Z \to X$ that are continuous on a set $s \subseteq Z$, the evaluation function $z \mapsto f(z)(g(z))$ is also continuous on $s$.