hasDerivAt_iff_hasFDerivAt — Mathlib

English

Let f: 𝕜 → F. Then f has a (non‑strict) derivative f' at x if and only if f has a Fréchet derivative at x given by the linear map h ↦ h f'.

Русский

Пусть f: 𝕜 → F. Тогда существует производная в точке x в смысле обычной производной эквивалентна существованию Фреше-производной, задаваемой линейным отображением h ↦ h f'.

LaTeX

$$$\\mathrm{HasDerivAt}(f,f',x) \\iff \\mathrm{HasFDerivAt}\\left(f, (h \\mapsto h\,f'), x\\right).$$$

Lean4

/-- Expressing `HasDerivAt f f' x` in terms of `HasFDerivAt` -/
theorem hasDerivAt_iff_hasFDerivAt {f' : F} : HasDerivAt f f' x ↔ HasFDerivAt f (smulRight (1 : 𝕜 →L[𝕜] 𝕜) f') x :=
  Iff.rfl

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