isBoundedBilinearMap_smul — Mathlib

English

If 𝕜' is a normed field and 𝕜-algebra, then the map (a, x) ↦ a · x from 𝕜' × E to E is a bounded bilinear map.

Русский

Если 𝕜' — нормированное поле, являющееся нормированным алгеброидами над 𝕜, то отображение (a, x) ↦ a · x: 𝕜' × E → E является ограниченным билинейным отображением.

LaTeX

$$$IsBoundedBilinearMap 𝕜 \bigl(p \mapsto p.1 \cdot p.2\bigr)$$$

Lean4

theorem isBoundedBilinearMap_smul {𝕜' : Type*} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type*}
    [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :
    IsBoundedBilinearMap 𝕜 fun p : 𝕜' × E => p.1 • p.2 :=
  (lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] E →L[𝕜] E).isBoundedBilinearMap

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