hasFDerivAt_iff — Mathlib

English

Let f0 and f1 be maps from a normed space E to F, and suppose they coincide in a neighborhood of x. Then f0 is Fréchet differentiable at x with derivative f' if and only if f1 is Fréchet differentiable at x with the same derivative.

Русский

Пусть f0 и f1: E → F, и пусть они совпадают в некоторой окрестности точки x. Тогда f0 зависит Фреше-дифференцируемо в точке x с производной f' тогда и только тогда, когда f1 дифференцируема в x с той же производной.

LaTeX

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

Lean4

theorem hasFDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) : HasFDerivAt f₀ f' x ↔ HasFDerivAt f₁ f' x :=
  h.hasFDerivAtFilter_iff h.eq_of_nhds fun _ => _root_.rfl

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