English
If f: X → L(E,G) is continuous on a set s and g: X → E is continuous on s, then x ↦ f(x)(g(x)) is continuous on s.
Русский
Пусть f: X → L(E,G) непрерывно на s, и g: X → E непрерывно на s; тогда x ↦ f(x)(g(x)) непрерывно на s.
LaTeX
$$$f: X \to L(E,G),\; g: X \to E,\; s\subseteq X;\; f\text{ непрерывно на }s,\; g\text{ непрерывно на }s\Rightarrow x \mapsto f(x)(g(x))\text{ непрерывно на }s.$$$
Lean4
theorem clm_apply {f : X → E →L[𝕜] F} {g : X → E} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
ContinuousOn (fun x ↦ f x (g x)) s :=
isBoundedBilinearMap_apply.continuous.comp_continuousOn (hf.prodMk hg)