fderivWithin — Mathlib

English

For q ∈ Polynomial R and hxs, fderivWithin 𝕜 (λ x, aeval x q) s x equals aeval x (derivative q).

Русский

Для q ∈ Polynomial R и hxs, fderivWithin 𝕜 (λ x, aeval x q) s x равно aeval x (derivative q).

LaTeX

$$$fderivWithin\_\{\mathbb{K}\}\left(\lambda x, aeval x q\right) s x = aeval x (derivative q)$$$

Lean4

protected theorem fderivWithin (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun x => p.eval x) s x = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (p.derivative.eval x) :=
  (p.hasFDerivWithinAt x).fderivWithin hxs

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