isBoundedLinearMap_deriv — Mathlib

English

For a finite type ι with normed spaces E i, the bilinear map (g, h) ↦ g.compContinuousMultilinearMap h is bounded.

Русский

Для конечного типа ι с нормированными пространствами E i, билинейное отображение (g,h) ↦ g.compContinuousMultilinearMap h ограничено.

LaTeX

$$$IsBoundedBilinearMap 𝕜 (\lambda p: (F →L[𝕜] G) × ContinuousMultilinearMap 𝕜 E F, p.1.compContinuousMultilinearMap p.2)$$$

Lean4

/-- Given a bounded bilinear map `f`, the map associating to a point `p` the derivative of `f` at
`p` is itself a bounded linear map. -/
theorem isBoundedLinearMap_deriv (h : IsBoundedBilinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 fun p : E × F => h.deriv p :=
  h.toContinuousLinearMap.deriv₂.isBoundedLinearMap

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