hasDerivWithinAt — Mathlib

English

For p ∈ 𝕜[X], the derivative within any set s of the function x ↦ p.eval x at x is p.derivative.eval x.

Русский

Для p ∈ 𝕜[X] производная внутри произвольного множества s от функции x ↦ p.eval x в точке x равна p.derivative.eval x.

LaTeX

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

Lean4

protected theorem hasDerivWithinAt (x : 𝕜) (s : Set 𝕜) :
    HasDerivWithinAt (fun x => p.eval x) (p.derivative.eval x) s x :=
  (p.hasDerivAt x).hasDerivWithinAt

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