isBoundedLinearMap_left — Mathlib

English

For a bilinear map h, fixing y, the map x ↦ f(x,y) is a bounded linear map.

Русский

Для билинейного отображения при фиксированном y отображение x ↦ f(x,y) ограничено и линейно.

LaTeX

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

Lean4

theorem isBoundedLinearMap_left (h : IsBoundedBilinearMap 𝕜 f) (y : F) : IsBoundedLinearMap 𝕜 fun x => f (x, y) :=
  (h.toContinuousLinearMap.flip y).isBoundedLinearMap

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