English
If x ∉ mulTSupport f, then ContMDiffWithinAt I I' n f s x holds for all s and n.
Русский
Если x ∉ mulTSupport(f), то ContMDiffWithinAt I I' n f s x выполняется для любых s и n.
LaTeX
$$$Not( x \in mulTSupport(f) ) \Rightarrow ∀ n s, ContMDiffWithinAt_I_I'_n f s x$$
Lean4
@[to_additive contMDiffWithinAt_of_notMem]
theorem contMDiffWithinAt_of_notMem_mulTSupport {f : M → M'} [One M'] {x : M} (hx : x ∉ mulTSupport f) (n : WithTop ℕ∞)
(s : Set M) : ContMDiffWithinAt I I' n f s x := by
apply
contMDiffWithinAt_const.congr_of_eventuallyEq
(eventually_nhdsWithin_of_eventually_nhds <| notMem_mulTSupport_iff_eventuallyEq.mp hx)
(image_eq_one_of_notMem_mulTSupport hx)