differentiableAt_iff — Mathlib

English

If f0 and f1 agree near x, then f0 is differentiable at x with some derivative f' if and only if f1 is differentiable at x with the same derivative.

Русский

Если f0 и f1 совпадают в окрестности точки x, то существование производной Фреше у f0 в x с производной f' эквивалентно существованию такой же производной у f1 в x.

LaTeX

$$$ \\mathrm{HasFDerivAt}(f_0,f',x) \\iff \\mathrm{HasFDerivAt}(f_1,f',x) $$$

Lean4

theorem differentiableAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) : DifferentiableAt 𝕜 f₀ x ↔ DifferentiableAt 𝕜 f₁ x :=
  exists_congr fun _ => h.hasFDerivAt_iff

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