differentiableWithinAt_aeval — Mathlib

English

For any q ∈ R[X], x ∈ 𝕜 and set s, x ↦ aeval x q is differentiable within s at x.

Русский

Пусть q ∈ R[X], x ∈ 𝕜 и s — множество. Тогда x ↦ aeval x q дифференцируема внутри s в x.

LaTeX

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

Lean4

protected theorem differentiableWithinAt_aeval : DifferentiableWithinAt 𝕜 (fun x => aeval x q) s x :=
  q.differentiableAt_aeval.differentiableWithinAt

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