hasStrictDerivAt_aeval — Mathlib

English

Variant articulation of the strict derivative of aeval x q.

Русский

Вариант формулировки строгой производной от aeval x q.

LaTeX

$$$Polynomial.hasStrictDerivAt\\_aeval (x) : HasStrictDerivAt\$\\lambda x. aeval x q\$\\left( aeval x (derivative q)\\right) x$$$

Lean4

protected theorem hasStrictDerivAt_aeval (x : 𝕜) : HasStrictDerivAt (fun x => aeval x q) (aeval x (derivative q)) x :=
  by simpa only [aeval_def, eval₂_eq_eval_map, derivative_map] using (q.map (algebraMap R 𝕜)).hasStrictDerivAt x

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