contDiffOn — Mathlib

English

If f is C^n at x, then for any m ≤ n there exists a neighborhood u of x on which f is C^m.

Русский

Если функция f является C^n в точке x, то для любого m ≤ n существует окрестность u точки x, на которой f является C^m.

LaTeX

$$$ContDiffAt\ 𝕜\ n\ f\ x\,\land\, m \le n\,\land\, (m = \infty \rightarrow n = ω)\Rightarrow \exists u\in 𝓝 x,\ ContDiffOn\ 𝕜\ m\ f\ u$$$

Lean4

nonrec theorem contDiffOn (h : ContDiffAt 𝕜 n f x) (hm : m ≤ n) (h' : m = ∞ → n = ω) : ∃ u ∈ 𝓝 x, ContDiffOn 𝕜 m f u :=
  by simpa [nhdsWithin_univ] using h.contDiffOn hm h'

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