clm_apply — Mathlib

English

If f and g are continuous at a point x, then the map x ↦ f(x)(g(x)) is continuous at x.

Русский

Если f и g непрерывны в точке x, то x ↦ f(x)(g(x)) непрерывно в x.

LaTeX

$$$f: X \to E \toL[G],\; g: X \to E,\; x \in X;\; f\text{ непрерывно в }x\text{ и } g\text{ непрерывно в }x\Rightarrow x\mapsto f(x)(g(x))\text{ непрерывно в }x.$$$

Lean4

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

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