clm_apply — Mathlib

English

If f: X → L(E,G) and g: X → E are continuous on a set s, then x ↦ f(x)coprod g(x) is continuous on s.

Русский

Если f: X → L(E,G) и g: X → E непрерывны на s, то x ↦ f(x)coprod g(x) непрерывно на s.

LaTeX

$$$f: X \to L(E,G),\; g: X \to E,\; s\subseteq X;\; f,g\text{ ContinuousOn on }s\Rightarrow x \mapsto f(x)\coprod g(x)\text{ ContinuousOn on }s.$$$

Lean4

@[continuity, fun_prop]
theorem clm_apply {X} [TopologicalSpace X] {f : X → E →L[𝕜] F} {g : X → E} {s : Set X} {x : X}
    (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun x ↦ f x (g x)) s x :=
  isBoundedBilinearMap_apply.continuous.continuousAt.comp_continuousWithinAt (hf.prodMk hg)

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