mfderiv_eq — Mathlib

English

If two functions are equal in a neighborhood of x, their MF derivatives at x are equal.

Русский

Если две функции равны в окрестности точки x, их MF-дифференциалы в x равны.

LaTeX

$$$f_1 =^ {\\mathcal{N}x} f \\Rightarrow mfderiv I I' f_1 x = mfderiv I I' f x$$$

Lean4

theorem mfderiv_eq (hL : f₁ =ᶠ[𝓝 x] f) : mfderiv I I' f₁ x = mfderiv I I' f x :=
  by
  have A : f₁ x = f x := (mem_of_mem_nhds hL :)
  rw [← mfderivWithin_univ, ← mfderivWithin_univ]
  rw [← nhdsWithin_univ] at hL
  exact hL.mfderivWithin_eq A

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