contMDiffWithinAt_of_notMem_mulTSupport

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)

Похожие утверждения