English
Let s ⊆ T and t ⊆ X. If f: T → X → Y and g ∈ C(t, Y) and the uncurried f is continuous on s × t, then x ↦ mkD(t.restrict (f(x))) g is continuous on s.
Русский
Пусть s ⊆ T и t ⊆ X. Пусть f: T → X → Y, g ∈ C(t, Y) и uncurry f непрерывна на s × t. Тогда x ↦ mkD(t.restrict (f(x))) g непрерывно на s.
LaTeX
$$$\\operatorname{ContinuousOn}(\\operatorname{Function.uncurry} f)(s \\times t) \\Rightarrow \\operatorname{Continuous}\\left(\\lambda x, \\mathrm{mkD}(t\\restriction (f(x)))\, g\\right)\\, s$$
Lean4
theorem continuous_mkD_restrict_of_uncurry {t : Set X} (f : T → X → Y) (g : C(t, Y))
(f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)) : Continuous (fun x ↦ mkD (t.restrict (f x)) g) :=
by
have (x : _) : ContinuousOn (f x) t := f_cont.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨trivial, hz⟩
refine continuous_of_continuous_uncurry _ ?_
conv in mkD _ _ => rw [mkD_of_continuousOn (this x)]
exact f_cont.comp_continuous (.prodMap continuous_id continuous_subtype_val) fun xz ↦ ⟨trivial, xz.2.2⟩
