hasFDerivWithinAt — Mathlib

English

A bounded bilinear map h has a Fréchet derivative within u at p, with derivative h.deriv p.

Русский

Ограниченная билинейная карта h имеет внутри области u Фреше-производную в p, равную h.deriv p.

LaTeX

$$$\text{HasFDerivWithinAt}(h, h.deriv p, u, p)$$$

Lean4

@[fun_prop]
theorem hasFDerivWithinAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : HasFDerivWithinAt b (h.deriv p) u p :=
  (h.hasFDerivAt p).hasFDerivWithinAt

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