contDiff_one_iff_fderiv — Mathlib

English

A function is C^1 if and only if it is differentiable and its derivative is continuous.

Русский

Функция является C^1 тогда и только тогда, когда она дифференцируема и её производная непрерывна.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}}\ 1\ f \iff \big(\operatorname{Differentiable}_{\mathbb{K}} f \land \operatorname{Continuous}(fderiv_{\mathbb{K}} f)\big)$$$

Lean4

theorem contDiff_one_iff_fderiv : ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (fderiv 𝕜 f) :=
  by
  rw [← zero_add 1, contDiff_succ_iff_fderiv]
  simp

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