differentiableOn_aeval

Mathlib.Analysis.Calculus.Deriv.Polynomial

URI: https://scilib.ai/kg/mathlib#Polynomial.differentiableOn_aeval

English

For q ∈ Polynomial R, the map x ↦ aeval x q is differentiable on s.

Русский

Для q ∈ Polynomial R отображение x ↦ aeval x q дифференцируемо на множестве s.

LaTeX

$$$DifferentiableOn\_\{\mathbb{K}\}$\lambda x, aeval x q$ s$$

Lean4

protected theorem differentiableOn_aeval : DifferentiableOn 𝕜 (fun x => aeval x q) s :=
  q.differentiable_aeval.differentiableOn

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru