contDiff_one_iff_deriv — Mathlib

English

Infinite differentiability of a function is equivalent to infinite differentiability of its derivative.

Русский

Бесконечная дифференцируемость функции эквивалентна бесконечной гладкости её производной.

LaTeX

$$$contDiff\ 𝕜\ ∞ f_2 \iff contDiff\ 𝕜\ ∞ (deriv f_2)$$$

Lean4

theorem contDiff_one_iff_deriv : ContDiff 𝕜 1 f₂ ↔ Differentiable 𝕜 f₂ ∧ Continuous (deriv f₂) :=
  by
  rw [show (1 : WithTop ℕ∞) = 0 + 1 from rfl, contDiff_succ_iff_deriv]
  simp

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