continuous_deriv_one — Mathlib

English

If a function is C^2, then the derivative is differentiable and derivative is C^1.

Русский

Если функция C^2, то её производная дифференцируема и сама гладкая (C^1).

LaTeX

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

Lean4

@[fun_prop]
theorem continuous_deriv_one (h : ContDiff 𝕜 1 f₂) : Continuous (deriv f₂) :=
  ContDiff.continuous_deriv h (le_refl 1)

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