clm_apply — Mathlib

English

The operation of applying a continuous linear map chain, i.e., x ↦ g(x)(f(x)) is continuous when g and f are continuous.

Русский

Операция применения цепи непрерывных линейных отображений непрерывна, если f и g непрерывны.

LaTeX

$$$Continuous fun x => (g x).(f x)\;\text{(composition is continuous)}$$$

Lean4

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

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