English
If s and t coincide locally around y, then MDifferentiableWithinAt I I' f s x f' is equivalent to MDifferentiableWithinAt I I' f t x f'.
Русский
Если s и t совпадают локально вокруг y, то MDifferentiableWithinAt I I' f s x f' эквивалентно MDifferentiableWithinAt I I' f t x f'.
LaTeX
$$$$MDifferentiableWithinAt I I' f s x \\Rightarrow MDifferentiableWithinAt I I' f t x$$$$
Lean4
/-- If two sets coincide locally, except maybe at a point, then it is equivalent to have a manifold
derivative within one or the other. -/
theorem hasMFDerivWithinAt_congr_set' (y : M) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
HasMFDerivWithinAt I I' f s x f' ↔ HasMFDerivWithinAt I I' f t x f' :=
by
have : T1Space M := I.t1Space M
simp only [HasMFDerivWithinAt]
refine and_congr ?_ ?_
· exact continuousWithinAt_congr_set' _ h
· apply hasFDerivWithinAt_congr_set' (extChartAt I x x)
exact preimage_extChartAt_eventuallyEq_compl_singleton y h
