hasStrictDerivAt — Mathlib

English

If HasFPowerSeriesAt f p x, then f′(x) equals p(1) applied to the constant function 1.

Русский

Если у функции f есть разложение в ряд ФПС около x с коэффициентами p, то производная в точке x равна p(1) применяемому к константной функции 1.

LaTeX

$$$HasFPowerSeriesAt f p x \Rightarrow deriv f x = p 1 (\lambda _ . 1)$$$

Lean4

protected theorem hasStrictDerivAt (h : HasFPowerSeriesAt f p x) : HasStrictDerivAt f (p 1 fun _ => 1) x :=
  h.hasStrictFDerivAt.hasStrictDerivAt

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