congr_of_eventuallyEq — Mathlib

English

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

Русский

Если f имеет MF-дериватив в x с производной f' и f1 эквивалентно f почти во всех окрестностях x, то у f1 тот же MF-дериватив в x.

LaTeX

$$$HasMFDerivAt\ I I'\ f\ x\ f' \land f_1 =^\smallfrown_{\mathcal{N}[ } f \Rightarrow HasMFDerivAt\ I I'\ f\ x\ f'$$$

Lean4

theorem congr_of_eventuallyEq (h : HasMFDerivAt I I' f x f') (h₁ : f₁ =ᶠ[𝓝 x] f) : HasMFDerivAt I I' f₁ x f' :=
  by
  rw [← hasMFDerivWithinAt_univ] at h ⊢
  apply h.congr_of_eventuallyEq _ (mem_of_mem_nhds h₁ :)
  rwa [nhdsWithin_univ]

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