English
The property ContMDiffWithinAt is invariant under replacing a function by another that agrees on a target set: ContMDiffWithinAt I I' n f1 s x holds iff ContMDiffWithinAt I I' n f s x holds when f1 and f agree on s.
Русский
Свойство ContMDiffWithinAt инвариантно при замене функции на другую, которая совпадает на заданном множестве: ContMDiffWithinAt I I' n f1 s x существует тогда и только тогда, когда ContMDiffWithinAt I I' n f s x существует при условии, что f1 и f совпадают на s.
LaTeX
$$$(\forall y \in s, f_1 y = f y) \Rightarrow (ContMDiffWithinAt I I' n f_1 s x) \Leftrightarrow (ContMDiffWithinAt I I' n f s x).$$$
Lean4
theorem contMDiffWithinAt_iff (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x :=
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff_of_eventuallyEq h₁ hx
