isBoundedLinearMap_comp_left — Mathlib

English

The bilinear map p ↦ p.fst.comp p.snd from (F →L G) × (E →L F) to E →L G is bounded.

Русский

Билинейное отображение p ↦ p.fst.comp p.snd из (F →L G) × (E →L F) в E →L G ограничено.

LaTeX

$$$IsBoundedBilinearMap 𝕜 \bigl(p \mapsto p.fst.comp p.snd\bigr)$$$

Lean4

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

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