hasFDerivWithinAt — Mathlib

English

For p ∈ 𝕜[X], x ∈ 𝕜, HasDerivWithinAt (fun x => p.eval x) (p.derivative.eval x) s x

Русский

Для p ∈ 𝕜[X], x ∈ 𝕜, HasDerivWithinAt от x ↦ p.eval x равна p.derivative.eval x внутри s

LaTeX

$$$HasDerivWithinAt\left(\lambda x, p.eval\ x\right)\left( p.derivative.eval x\right) s x$$$

Lean4

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

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