English
For any y ∈ M, adding y to the domain set does not change differentiability within at x. That is, differentiability within at x on insert y s is equivalent to differentiability within at x on s.
Русский
Для любого y ∈ M добавление y к области определения не меняет дифференцируемость внутри x. То есть дифференцируемость внутри x на insert y s эквивалентна дифференцируемости на s.
LaTeX
$$$$MDifferentiableWithinAt I I' f (insert y s) x \\iff MDifferentiableWithinAt I I' f s x$$$$
Lean4
theorem mdifferentiableWithinAt_insert {y : M} :
MDifferentiableWithinAt I I' f (insert y s) x ↔ MDifferentiableWithinAt I I' f s x :=
by
rcases eq_or_ne x y with (rfl | h)
· exact mdifferentiableWithinAt_insert_self
have : T1Space M := I.t1Space M
apply mdifferentiableWithinAt_congr_nhds
exact nhdsWithin_insert_of_ne h
