English
Let X, Y, T be topological spaces. If f: T → X → Y and g ∈ C(X, Y) with the uncurried version of f continuous, then the map t ↦ mkD(f(t)) g is a continuous map from T into C(X, Y).
Русский
Пусть X, Y, T — топологические пространства. Пусть f: T → X → Y и g ∈ C(X, Y), причем функция uncurry f непрерывна. Тогда отображение t ↦ mkD(f(t)) g непрерывно как отображение T в C(X, Y).
LaTeX
$$$\\operatorname{Continuous}(\\operatorname{Function.uncurry} f) \\Rightarrow \\operatorname{Continuous}\\left( t \\mapsto \\mathrm{mkD}\\bigl(f(t)\\bigr)\\, g \\right)$$$
Lean4
/-- A variant of `ContinuousMap.continuous_of_continuous_uncurry` in terms of
`ContinuousMap.mkD`.
Of course, in this particular setting, `fun x ↦ mkD (f x) g` is just `f`,
but the `mkD` spelling appears naturally in the context of `C(α, β)`-valued integration. -/
theorem continuous_mkD_of_uncurry (f : T → X → Y) (g : C(X, Y)) (f_cont : Continuous (Function.uncurry f)) :
Continuous (fun x ↦ mkD (f x) g) :=
by
have (x : _) : Continuous (f x) := f_cont.comp (Continuous.prodMk_right x)
refine continuous_of_continuous_uncurry _ ?_
conv in mkD _ _ => rw [mkD_of_continuous (this x)]
exact f_cont
