English
Let s ⊆ T and t ⊆ X. If f: T → X → Y and g ∈ C(t, Y) and f_cont : ContinuousOn (Function.uncurry f) (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) и f_cont: ContinuousOn (Function.uncurry f) на s × t. Тогда x ↦ mkD (t.restrict (f x)) g непрерывно на s.
LaTeX
$$$\\operatorname{ContinuousOn}(\\operatorname{Function.uncurry} f)(s \\times t) \\Rightarrow \\operatorname{ContinuousOn}\\bigl(\\lambda x, \\mathrm{mkD}(t\\restriction (f(x)))\\, g\\bigr)\\, s$$$
Lean4
theorem continuousOn_mkD_restrict_of_uncurry {s : Set T} {t : Set X} (f : T → X → Y) (g : C(t, Y))
(f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)) : ContinuousOn (fun x ↦ mkD (t.restrict (f x)) g) s :=
by
have (x) (hx : x ∈ s) : ContinuousOn (f x) t :=
f_cont.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨hx, hz⟩
simp_rw [continuousOn_iff_continuous_restrict, s.restrict_def]
refine continuous_of_continuous_uncurry _ ?_
conv in mkD _ _ => rw [mkD_of_continuousOn (this x x.2)]
exact f_cont.comp_continuous (.prodMap continuous_subtype_val continuous_subtype_val) fun xz ↦ ⟨xz.1.2, xz.2.2⟩
