contMDiffAt_of_notMem_mulTSupport

English

If f is C^n at every point in mulTSupport f, then f is C^n everywhere.

Русский

Если f ∈mulTSupport имеет C^n гладкость в каждой точке, то f ∈ C^n по всей области.

LaTeX

$$$\forall x \in mulTSupport(f), ContMDiffAt I I' n f x \Rightarrow ContMDiff I I' n f$$$

Lean4

/-- `f` is continuously differentiable at each point outside of its `mulTSupport`. -/
@[to_additive contMDiffAt_of_notMem]
theorem contMDiffAt_of_notMem_mulTSupport {f : M → M'} [One M'] {x : M} (hx : x ∉ mulTSupport f) (n : WithTop ℕ∞) :
    ContMDiffAt I I' n f x :=
  contMDiffWithinAt_of_notMem_mulTSupport hx n univ

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