isBoundedLinearMap_comp_right — Mathlib

English

For g ∈ F →L G, the map f ↦ g ∘ f is a bounded linear map from E →L F to G.

Русский

Для g ∈ F →L G отображение f ↦ g ∘ f является ограниченным линейным отображением от E →L F в G.

LaTeX

$$$IsBoundedLinearMap 𝕜 (\lambda f: E →L[𝕜] F, ContinuousLinearMap.comp g f)$$$

Lean4

theorem isBoundedLinearMap_comp_right (f : E →L[𝕜] F) :
    IsBoundedLinearMap 𝕜 fun g : F →L[𝕜] G => ContinuousLinearMap.comp g f :=
  isBoundedBilinearMap_comp.isBoundedLinearMap_left _

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