deriv'

Mathlib.Analysis.Calculus.ContDiff.Basic

URI: https://scilib.ai/kg/mathlib#ContDiff.deriv'

English

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

Русский

Если f — C^2, то производная f дифференцируема.

LaTeX

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

Lean4

@[fun_prop]
theorem deriv' (h : ContDiff 𝕜 (n + 1) f₂) : ContDiff 𝕜 n (deriv f₂) := by unfold deriv; fun_prop

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

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

Разделы

Аффилиация

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