contDiff_one_iff_hasFDerivAt — Mathlib

English

A function is C^1 if and only if there exists a continuous f' : E → (E →L[𝕜] F) such that f'(x) is the derivative of f at x for all x.

Русский

Функция является C^1 тогда и только тогда существует непрерывное отображение f' : E → (E →L[𝕜] F), такое что f'(x) — производная f в точке x.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}}(1)\ f \iff \exists f': E \to (E \to_L[\mathbb{K}] F), \ \operatorname{Continuous}\ f'\land \forall x,\ HasFDerivAt\ f\ (f'(x))\ x$$$

Lean4

theorem contDiff_one_iff_hasFDerivAt :
    ContDiff 𝕜 1 f ↔ ∃ f' : E → E →L[𝕜] F, Continuous f' ∧ ∀ x, HasFDerivAt f (f' x) x := by
  convert contDiff_succ_iff_hasFDerivAt using 4; simp

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