congr_of_eventuallyEq — Mathlib

English

If h : HasDerivAt f f' x and nhdsWithin-like equality f1 ≈ f near x, then HasDerivAt f1 f' x.

Русский

Если у f есть производная f' в x, а f1 совпадает с f около x, тогда HasDerivAt f1 f' x.

LaTeX

$$$HasDerivAt f f' x \\rightarrow (nhds x).EventuallyEq f_1 f \\rightarrow HasDerivAt f_1 f' x$$$

Lean4

theorem congr_of_eventuallyEq (h : HasDerivAt f f' x) (h₁ : f₁ =ᶠ[𝓝 x] f) : HasDerivAt f₁ f' x :=
  HasDerivAtFilter.congr_of_eventuallyEq h h₁ (mem_of_mem_nhds h₁ :)

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