hasDerivWithinAt_aeval — Mathlib

English

Let q ∈ R[X]. For x ∈ 𝕜 and s ⊆ 𝕜, the derivative within s of x ↦ aeval x q equals aeval x (derivative q).

Русский

Пусть q ∈ R[X]. Для x ∈ 𝕜 и s ⊆ 𝕜 производная внутри s от x ↦ aeval x q равна aeval x (derivative q).

LaTeX

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

Lean4

protected theorem hasDerivWithinAt_aeval (x : 𝕜) (s : Set 𝕜) :
    HasDerivWithinAt (fun x => aeval x q) (aeval x (derivative q)) s x :=
  (q.hasDerivAt_aeval x).hasDerivWithinAt

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