English
Let s ⊆ T, f: T → X → Y, g ∈ C(X, Y). If the uncurried f is continuous on s × univ, then x ↦ mkD(f(x)) g is continuous on s.
Русский
Пусть s ⊆ T, f: T → X → Y, g ∈ C(X, Y). Если uncurry f непрерывна на s × univ, то отображение x ↦ mkD(f(x)) g непрерывно на s.
LaTeX
$$$\\operatorname{ContinuousOn}(\\operatorname{Function.uncurry} f)(s \\times \\operatorname{univ}) \\Rightarrow \\operatorname{ContinuousOn}\\bigl(\\lambda x, \\mathrm{mkD}(f(x))\, g\\bigr)\\, s$$$
Lean4
theorem continuousOn_mkD_of_uncurry {s : Set T} (f : T → X → Y) (g : C(X, Y))
(f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)) : ContinuousOn (fun x ↦ mkD (f x) g) s :=
by
have (x) (hx : x ∈ s) : Continuous (f x) := f_cont.comp_continuous (Continuous.prodMk_right x) fun _ ↦ ⟨hx, trivial⟩
simp_rw [continuousOn_iff_continuous_restrict, s.restrict_def]
refine continuous_of_continuous_uncurry _ ?_
conv in mkD _ _ => rw [mkD_of_continuous (this x x.2)]
exact f_cont.comp_continuous (.prodMap continuous_subtype_val continuous_id) fun xz ↦ ⟨xz.1.2, trivial⟩
