Bundled maps with evaluation continuous in both variables #
In this file we define a class ContinuousEval F X Y
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 u_1)
(X : outParam (Type u_2))
(Y : outParam (Type u_3))
[FunLike F X Y]
[TopologicalSpace F]
[TopologicalSpace X]
[TopologicalSpace Y]
:
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.
- continuous_eval : Continuous fun (fx : F × X) => fx.1 fx.2
Evaluation of a bundled morphism at a point is continuous in both variables.
Instances
theorem
Continuous.eval
{F : Type u_1}
{X : Type u_2}
{Y : Type u_3}
{Z : Type u_4}
[FunLike F X Y]
[TopologicalSpace F]
[TopologicalSpace X]
[TopologicalSpace Y]
[ContinuousEval F X Y]
[TopologicalSpace Z]
{f : Z → F}
{g : Z → X}
(hf : Continuous f)
(hg : Continuous g)
:
Continuous fun (z : Z) => (f z) (g z)
theorem
ContinuousEval.of_continuous_forget
{F : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[FunLike F X Y]
[TopologicalSpace F]
[TopologicalSpace X]
[TopologicalSpace Y]
[ContinuousEval F X Y]
{F' : Type u_5}
[FunLike F' X Y]
[TopologicalSpace F']
{f : F' → F}
(hc : Continuous f)
(hf : ∀ (g : F'), ⇑(f g) = ⇑g := by intro; rfl)
:
ContinuousEval F' X Y
If a type F' of bundled morphisms admits a continuous projection
to a type satisfying ContinuousEval,
then F' satisfies this predicate too.
The word "forget" in the name is motivated by the term "forgetful functor".
@[instance 100]
instance
ContinuousEval.toContinuousMapClass
{F : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[FunLike F X Y]
[TopologicalSpace F]
[TopologicalSpace X]
[TopologicalSpace Y]
[ContinuousEval F X Y]
:
ContinuousMapClass F X Y
@[instance 100]
instance
ContinuousEval.toContinuousEvalConst
{F : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[FunLike F X Y]
[TopologicalSpace F]
[TopologicalSpace X]
[TopologicalSpace Y]
[ContinuousEval F X Y]
:
ContinuousEvalConst F X Y
theorem
Filter.Tendsto.eval
{F : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[FunLike F X Y]
[TopologicalSpace F]
[TopologicalSpace X]
[TopologicalSpace Y]
[ContinuousEval F X Y]
{α : Type u_5}
{l : Filter α}
{f : α → F}
{f₀ : F}
{g : α → X}
{x₀ : X}
(hf : Filter.Tendsto f l (nhds f₀))
(hg : Filter.Tendsto g l (nhds x₀))
:
Filter.Tendsto (fun (a : α) => (f a) (g a)) l (nhds (f₀ x₀))
theorem
ContinuousAt.eval
{F : Type u_1}
{X : Type u_2}
{Y : Type u_3}
{Z : Type u_4}
[FunLike F X Y]
[TopologicalSpace F]
[TopologicalSpace X]
[TopologicalSpace Y]
[ContinuousEval F X Y]
[TopologicalSpace Z]
{f : Z → F}
{g : Z → X}
{z : Z}
(hf : ContinuousAt f z)
(hg : ContinuousAt g z)
:
ContinuousAt (fun (z : Z) => (f z) (g z)) z
theorem
ContinuousWithinAt.eval
{F : Type u_1}
{X : Type u_2}
{Y : Type u_3}
{Z : Type u_4}
[FunLike F X Y]
[TopologicalSpace F]
[TopologicalSpace X]
[TopologicalSpace Y]
[ContinuousEval F X Y]
[TopologicalSpace Z]
{f : Z → F}
{g : Z → X}
{s : Set Z}
{z : Z}
(hf : ContinuousWithinAt f s z)
(hg : ContinuousWithinAt g s z)
:
ContinuousWithinAt (fun (z : Z) => (f z) (g z)) s z
theorem
ContinuousOn.eval
{F : Type u_1}
{X : Type u_2}
{Y : Type u_3}
{Z : Type u_4}
[FunLike F X Y]
[TopologicalSpace F]
[TopologicalSpace X]
[TopologicalSpace Y]
[ContinuousEval F X Y]
[TopologicalSpace Z]
{f : Z → F}
{g : Z → X}
{s : Set Z}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (fun (z : Z) => (f z) (g z)) s