mulLeftRight_isBoundedBilinear — Mathlib

English

The map p ↦ ContinuousLinearMap.mulLeftRight p.1 p.2 is a bounded bilinear map, i.e., the tensor product of left and right multiplications is bounded.

Русский

Отображение p ↦ ContinuousLinearMap.mulLeftRight p.1 p.2 является ограниченным билинейным отображением.

LaTeX

$$$IsBoundedBilinearMap 𝕜 (\lambda p: 𝕜' × 𝕜', ContinuousLinearMap.mulLeftRight 𝕜 p.1 p.2)$$$

Lean4

/-- The function `ContinuousLinearMap.mulLeftRight : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜')` is a bounded
bilinear map. -/
theorem mulLeftRight_isBoundedBilinear (𝕜' : Type*) [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] :
    IsBoundedBilinearMap 𝕜 fun p : 𝕜' × 𝕜' => ContinuousLinearMap.mulLeftRight 𝕜 𝕜' p.1 p.2 :=
  (ContinuousLinearMap.mulLeftRight 𝕜 𝕜').isBoundedBilinearMap

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