contMDiffAt_iff_contMDiffOn_nhds — Mathlib

English

For n finite, ContMDiffAt at x is equivalent to the existence of a neighborhood where ContMDiffOn holds.

Русский

Для конечного n ContMDiffAt в точке x эквивалентно существованию окрестности, на которой ContMDiffOn держится.

LaTeX

$$$ ContMDiffAt I I' n f x \iff ∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u $$$

Lean4

/-- A function is `C^n` at a point, for `n : ℕ`, if and only if it is `C^n` on
a neighborhood of this point. -/
theorem contMDiffAt_iff_contMDiffOn_nhds [IsManifold I n M] [IsManifold I' n M'] (hn : n ≠ ∞) :
    ContMDiffAt I I' n f x ↔ ∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u := by
  simp [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_contMDiffOn_nhds hn, nhdsWithin_univ]

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