congr_of_eventuallyEq — Mathlib

English

If f has differentiable at x with MF-derivative, and f1 equals f near x, then f1 is differentiable at x with the same MF-derivative.

Русский

Если f дифференцируемо в x с MF-деривативом, и f1 близко к f в окрестности x, то f1 дифференцируемо в x с тем же MF-деривативом.

LaTeX

$$$MDifferentiableAt I I' f x \land (nhds x).EventuallyEq f_1 f \Rightarrow MDifferentiableAt I I' f_1 x$$$

Lean4

theorem congr_of_eventuallyEq (h : MDifferentiableAt I I' f x) (hL : f₁ =ᶠ[𝓝 x] f) : MDifferentiableAt I I' f₁ x :=
  (h.hasMFDerivAt.congr_of_eventuallyEq hL).mdifferentiableAt

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