clm_apply — Mathlib

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)

Похожие утверждения