toContinuousLinearMap — Mathlib

English

If h is IsBoundedBilinearMap 𝕜 f, then for each y ∈ F the map x ↦ f(x,y) is bounded linear on E.

Русский

Если h — ограниченное билинейное отображение f, то для каждого y ∈ F отображение x ↦ f(x,y) ограничено линейно на E.

LaTeX

$$$IsBoundedBilinearMap\ 𝕜 f \Rightarrow \forall y\; IsBoundedLinearMap 𝕜 (\lambda x => f(x,y))$$$

Lean4

/-- A bounded bilinear map `f : E × F → G` defines a continuous linear map
`f : E →L[𝕜] F →L[𝕜] G`. -/
def toContinuousLinearMap (hf : IsBoundedBilinearMap 𝕜 f) : E →L[𝕜] F →L[𝕜] G :=
  LinearMap.mkContinuousOfExistsBound₂ (LinearMap.mk₂ _ f.curry hf.add_left hf.smul_left hf.add_right hf.smul_right) <|
    hf.bound.imp fun _ ↦ And.right

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