differentiable_deriv_two

Mathlib.Analysis.Calculus.ContDiff.Basic

URI: https://scilib.ai/kg/mathlib#ContDiff.differentiable_deriv_two

English

If f is C^2, then the derivative operator is differentiable.

Русский

Если f — C^2, то оператор дифференцирования гладкий.

LaTeX

$$$ContDiff\ 𝕜\ 2\ f_2 \Rightarrow Differentiable\ 𝕜 (deriv f_2)$$$

Lean4

@[fun_prop]
theorem differentiable_deriv_two (h : ContDiff 𝕜 2 f₂) : Differentiable 𝕜 (deriv f₂) := by unfold deriv; fun_prop

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

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

Разделы

Аффилиация

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