English
A C^1 function at x is equivalent to the existence of a derivative map f' at x that is continuous on a neighborhood and HasFDerivAt everywhere on that neighborhood.
Русский
C^1 в точке x эквивалентно существованию гомоморфной производной f' в окрестности x с непрерывностью и HasFDerivAt.
LaTeX
$$$contDiffAt_one_iff : ContDiffAt 𝕜 1 f x\iff \exists f' : E \to E \toL[𝕜] F, \exists u \in 𝓝 x, ContinuousOn f' u ∧ \forall y \in u, HasFDerivAt f (f' y) y$$$
Lean4
theorem contDiffAt_one_iff :
ContDiffAt 𝕜 1 f x ↔ ∃ f' : E → E →L[𝕜] F, ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x :=
by
rw [show (1 : WithTop ℕ∞) = (0 : ℕ) + 1 from rfl]
simp_rw [contDiffAt_succ_iff_hasFDerivAt, show ((0 : ℕ) : WithTop ℕ∞) = 0 from rfl, contDiffAt_zero,
exists_mem_and_iff antitone_bforall antitone_continuousOn, and_comm]
