clm_comp — Mathlib

English

The map p ↦ h.deriv p is a bounded linear map when h is a bounded bilinear map.

Русский

Когда h — ограниченное билинейное отображение, отображение p ↦ h.deriv p является ограниченным линейным отображением.

LaTeX

$$$IsBoundedLinearMap 𝕜 (\lambda p: E × F, h.deriv p)$$$

Lean4

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

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