English
Let f: E → F. Then f is C^(n+1) if and only if there exists a map f' from E to the space of continuous linear maps E →L[𝕜] F, such that f' is C^n and for every x, HasFDerivAt f at x equals f'(x).
Русский
Пусть f: E → F. Тогда f является C^(n+1), эквивалентно тому, что существует отображение f' : E → (E →L[𝕜] F), которое является C^n, и для каждого x функция f имеет производную HasFDerivAt f at x равную f'(x).
LaTeX
$$$\operatorname{ContDiff}_{\mathbb{K}}(n+1)\ f \iff \exists f': E \to (E \to_L[\mathbb{K}] F), \ \operatorname{ContDiff}_{\mathbb{K}}(n)\ f' \land \forall x,\ HasFDerivAt\ f\ (f'(x))\ x$$$
Lean4
/-- A function is `C^(n+1)` iff it has a `C^n` derivative. -/
theorem contDiff_succ_iff_hasFDerivAt {n : ℕ} :
ContDiff 𝕜 (n + 1) f ↔ ∃ f' : E → E →L[𝕜] F, ContDiff 𝕜 n f' ∧ ∀ x, HasFDerivAt f (f' x) x := by
simp only [← contDiffOn_univ, ← hasFDerivWithinAt_univ, Set.mem_univ, forall_true_left,
contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn uniqueDiffOn_univ, WithTop.natCast_ne_top, analyticOn_univ,
false_implies, true_and]
