deriv — Mathlib

English

The map p ↦ f(p.fst)(p.snd) is a bounded bilinear map, i.e., evaluation of a bilinear form is bounded.

Русский

Оценка билинейной формы через p.fst и p.snd образует ограниченное билинейное отображение.

LaTeX

$$$IsBoundedBilinearMap 𝕜 (\lambda p: (E \to_L[𝕜] F) \times E, p.fst.p snd)$$$

Lean4

/-- The derivative of a bounded bilinear map at a point `p : E × F`, as a continuous linear map
from `E × F` to `G`. The statement that this is indeed the derivative of `f` is
`IsBoundedBilinearMap.hasFDerivAt` in `Analysis.Calculus.FDeriv`. -/
def deriv (h : IsBoundedBilinearMap 𝕜 f) (p : E × F) : E × F →L[𝕜] G :=
  h.toContinuousLinearMap.deriv₂ p

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