hasFDerivWithinAt_aeval — Mathlib

English

For q ∈ Polynomial R, x ∈ 𝕜 and s ⊆ 𝕜, HasDerivWithinAt (λ x, aeval x q) (aeval x (derivative q)) s x.

Русский

Для q ∈ Polynomial R, x ∈ 𝕜 и s ⊆ 𝕜, HasDerivWithinAt (λ x, aeval x q) (aeval x (derivative q)) s x.

LaTeX

$$$HasDerivWithinAt\left(\lambda x, aeval x q\right)\left( aeval x (derivative q)\right) s x$$$

Lean4

protected theorem hasFDerivWithinAt_aeval (x : 𝕜) :
    HasFDerivWithinAt (fun x => aeval x q) (smulRight (1 : 𝕜 →L[𝕜] 𝕜) (aeval x (derivative q))) s x :=
  (q.hasFDerivAt_aeval x).hasFDerivWithinAt

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