English
If f1 equals f near x in nhds, then differentiability at x of f1 is equivalent to differentiability at x of f.
Русский
Если f1 вблизи x совпадает с f в окрестности, то дифференцируемость в x для f1 эквивалентна дифференцируемости в x для f.
LaTeX
$$$MDifferentiableWithinAt I I' f s x \iff MDifferentiableWithinAt I I' f_1 s x$$$
Lean4
theorem mfderivWithin_eq (hL : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
mfderivWithin I I' f₁ s x = mfderivWithin I I' f s x :=
by
by_cases h : MDifferentiableWithinAt I I' f s x
· unfold mfderivWithin
simp only [h, (hL.mdifferentiableWithinAt_iff hx).1 h, ↓reduceIte, writtenInExtChartAt]
apply Filter.EventuallyEq.fderivWithin_eq; swap
· simp [hx]
filter_upwards [extChartAt_preimage_mem_nhdsWithin (I := I) hL] with y hy
simp only [preimage_setOf_eq, mem_setOf_eq] at hy
simp [-extChartAt, hy, hx]
· unfold mfderivWithin
rw [if_neg h, if_neg]
rwa [← hL.mdifferentiableWithinAt_iff hx]
