congr_of_eventuallyEq — Mathlib

English

If f has derivative f' within s at x, and f1 is eventually equal to f with respect to the nhds within s at x, and f1 x = f x, then f1 has derivative f' within s at x.

Русский

Если у f есть производная f′ внутри s в точке x, и f1 совпадает с f в окрестности nhdsWithin x s, и f1(x)=f(x), тогда у f1 та же производная f′ внутри s в x.

LaTeX

$$$HasDerivWithinAt f f' s x \\rightarrow (f_1 =^\\infty[\\mathcal{N}[s] x] f) \\rightarrow (f_1 x = f x) \\rightarrow HasDerivWithinAt f_1 f' s x$$$

Lean4

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

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