isBoundedBilinearMap_compMultilinear

English

The composition of a continuous linear map with a continuous multilinear map is a bounded bilinear operation.

Русский

Сочетание непрерывного линейного отображения с непрерывной многолинейной картой образует ограниченную билинейную операцию.

LaTeX

$$$IsBoundedBilinearMap 𝕜 (\lambda p: F →L[𝕜] G \times ContinuousMultilinearMap 𝕜 E F \mapsto p.1.compContinuousMultilinearMap p.2)$$$

Lean4

/-- The composition of a continuous linear map with a continuous multilinear map is a bounded
bilinear operation. -/
theorem isBoundedBilinearMap_compMultilinear {ι : Type*} {E : ι → Type*} [Fintype ι] [∀ i, NormedAddCommGroup (E i)]
    [∀ i, NormedSpace 𝕜 (E i)] :
    IsBoundedBilinearMap 𝕜 fun p : (F →L[𝕜] G) × ContinuousMultilinearMap 𝕜 E F =>
      p.1.compContinuousMultilinearMap p.2 :=
  (compContinuousMultilinearMapL 𝕜 E F G).isBoundedBilinearMap

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