English
If s and t coincide locally around x, then mfderivWithin I I' f s x equals mfderivWithin I I' f t x.
Русский
Если s и t совпадают локально вокруг x, то mfderivWithin I I' f s x равно mfderivWithin I I' f t x.
LaTeX
$$$$(h : s =^\\{ x \\} t) \\Rightarrow mfderivWithin I I' f s x = mfderivWithin I I' f t x$$$$
Lean4
/-- If two sets coincide locally, except maybe at a point, then derivatives within these sets
are the same. -/
theorem mfderivWithin_congr_set' (y : M) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
mfderivWithin I I' f s x = mfderivWithin I I' f t x :=
by
by_cases hx : MDifferentiableWithinAt I I' f s x
· simp only [mfderivWithin, hx, (mdifferentiableWithinAt_congr_set' y h).1 hx, ↓reduceIte]
apply fderivWithin_congr_set' (extChartAt I x x)
exact preimage_extChartAt_eventuallyEq_compl_singleton y h
· simp [mfderivWithin, hx, ← mdifferentiableWithinAt_congr_set' y h]
