isBoundedLinearMap_right — Mathlib

English

Let f: E × F → G be a bounded bilinear map. Then for each fixed x ∈ E, the function y ↦ f(x,y) is a bounded linear map from F to G.

Русский

Пусть f: E × F → G — ограниченное билинейное отображение. Тогда для каждого фиксированного x ∈ E отображение y ↦ f(x,y) является ограниченным линейным отображением из F в G.

LaTeX

$$$\\forall x \\in E,\\; f(x,\\cdot) \\in L(F,G)$$$

Lean4

theorem isBoundedLinearMap_right (h : IsBoundedBilinearMap 𝕜 f) (x : E) : IsBoundedLinearMap 𝕜 fun y => f (x, y) :=
  (h.toContinuousLinearMap x).isBoundedLinearMap

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