hasFDerivAt — Mathlib

English

For q ∈ Polynomial R and x ∈ 𝕜, the derivative (Fréchet derivative) of the map x ↦ aeval x q is the linear map sending h to h times aeval x (derivative q).

Русский

Для q ∈ Polynomial R и x ∈ 𝕜 производная Фреше от x ↦ aeval x q равна линейному отображению, умножающему на h, значения aeval x (derivative q).

LaTeX

$$$HasFDerivAt\left(\lambda x, aeval x q\right)\left( smulRight\ 1\, (aeval x (derivative q))\right) x$$$

Lean4

protected theorem hasFDerivAt (x : 𝕜) :
    HasFDerivAt (fun x => p.eval x) (smulRight (1 : 𝕜 →L[𝕜] 𝕜) (p.derivative.eval x)) x :=
  p.hasDerivAt x

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