congr_of_eventuallyEq — Mathlib

English

If f and f1 are Fréchet differentiable at x with the same derivative, and f1 equals f in a neighborhood of x, then HasFDerivAt f1 f' x holds.

Русский

Если f и f1 дифференцируемы в точке x с одной производной, а f1 совпадает с f в окрестности x, то HasFDerivAt f1 f' x выполняется.

LaTeX

$$$ \\mathrm{HasFDerivAt}(f,f',x) \\to (\\text{nhds }x \\text{ EventuallyEq } f_1 f) \\to \\mathrm{HasFDerivAt}(f_1,f',x) $$$

Lean4

theorem congr_of_eventuallyEq (h : HasFDerivWithinAt f f' s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    HasFDerivWithinAt f₁ f' s x :=
  HasFDerivAtFilter.congr_of_eventuallyEq h h₁ hx

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