English
If a function is differentiable on each set in a family (s_i) and each s_i is open, then it is differentiable on the union of all s_i.
Русский
Если функция дифференцируема на каждом множестве из семейства (s_i) и каждое s_i открыто, то она дифференцируема на объединении всех s_i.
LaTeX
$$$$\\left(\\forall i, MDifferentiableOn I I' f (s_i)\\right) \\rightarrow MDifferentiableOn I I' f (\\bigcup_i s_i)$$$$
Lean4
/-- If two sets coincide around a point (except possibly at a single point `y`), then it is
equivalent to be differentiable within one or the other set. -/
theorem mdifferentiableWithinAt_congr_set' (y : M) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) :
MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x :=
by
simp only [mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt]
exact exists_congr fun _ => hasMFDerivWithinAt_congr_set' _ h
