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.
class
ContinuousEvalConst
(F : Type u_1)
(α : outParam (Type u_2))
(X : outParam (Type u_3))
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
:
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.
- continuous_eval_const (x : α) : Continuous fun (f : F) => f x
Instances
theorem
ContinuousEvalConst.of_continuous_forget
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
{F' : Type u_5}
[FunLike F' α X]
[TopologicalSpace F']
{f : F' → F}
(hc : Continuous f)
(hf : ∀ (g : F'), ⇑(f g) = ⇑g := by intro; rfl)
:
ContinuousEvalConst F' α X
If a type F' of bundled morphisms admits a continuous projection
to a type satisfying ContinuousEvalConst,
then F' satisfies this predicate too.
The word "forget" in the name is motivated by the term "forgetful functor".
theorem
Continuous.eval_const
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
{Z : Type u_4}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
[TopologicalSpace Z]
{f : Z → F}
(hf : Continuous f)
(x : α)
:
Continuous fun (x_1 : Z) => (f x_1) x
theorem
continuous_coeFun
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
:
theorem
Continuous.coeFun
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
{Z : Type u_4}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
[TopologicalSpace Z]
{f : Z → F}
(hf : Continuous f)
:
Continuous fun (z : Z) => ⇑(f z)
theorem
Filter.Tendsto.eval_const
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
{ι : Type u_5}
{l : Filter ι}
{f : ι → F}
{g : F}
(hf : Tendsto f l (nhds g))
(a : α)
:
theorem
Filter.Tendsto.coeFun
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
{ι : Type u_5}
{l : Filter ι}
{f : ι → F}
{g : F}
(hf : Tendsto f l (nhds g))
:
theorem
ContinuousAt.eval_const
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
{Z : Type u_4}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
[TopologicalSpace Z]
{f : Z → F}
{z : Z}
(hf : ContinuousAt f z)
(x : α)
:
ContinuousAt (fun (x_1 : Z) => (f x_1) x) z
theorem
ContinuousAt.coeFun
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
{Z : Type u_4}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
[TopologicalSpace Z]
{f : Z → F}
{z : Z}
(hf : ContinuousAt f z)
:
ContinuousAt (fun (z : Z) => ⇑(f z)) z
theorem
ContinuousWithinAt.eval_const
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
{Z : Type u_4}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
[TopologicalSpace Z]
{f : Z → F}
{s : Set Z}
{z : Z}
(hf : ContinuousWithinAt f s z)
(x : α)
:
ContinuousWithinAt (fun (x_1 : Z) => (f x_1) x) s z
theorem
ContinuousWithinAt.coeFun
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
{Z : Type u_4}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
[TopologicalSpace Z]
{f : Z → F}
{s : Set Z}
{z : Z}
(hf : ContinuousWithinAt f s z)
:
ContinuousWithinAt (fun (z : Z) => ⇑(f z)) s z
theorem
ContinuousOn.eval_const
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
{Z : Type u_4}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
[TopologicalSpace Z]
{f : Z → F}
{s : Set Z}
(hf : ContinuousOn f s)
(x : α)
:
ContinuousOn (fun (x_1 : Z) => (f x_1) x) s
theorem
ContinuousOn.coeFun
{F : Type u_1}
{α : Type u_2}
{X : Type u_3}
{Z : Type u_4}
[FunLike F α X]
[TopologicalSpace F]
[TopologicalSpace X]
[ContinuousEvalConst F α X]
[TopologicalSpace Z]
{f : Z → F}
{s : Set Z}
(hf : ContinuousOn f s)
(x : α)
:
ContinuousOn (fun (x_1 : Z) => (f x_1) x) s