fderivWithin_eq — Mathlib

English

If nhdsWithin x s witnesses f1 equals f, then fderivWithin f1 s x = fderivWithin f s x.

Русский

Если nhdsWithin фиксирует, что f1 равна f, то fderivWithin f1 s x = fderivWithin f s x.

LaTeX

$$$ (nhdsWithin x s).\\text{EventuallyEq}(f_1,f) \\to \\mathrm{fderivWithin}(f_1,s,x) = \\mathrm{fderivWithin}(f,s,x) $$$

Lean4

theorem fderivWithin_eq (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x := by
  classical simp only [fderivWithin, DifferentiableWithinAt, hs.hasFDerivWithinAt_iff hx]

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