contDiffOn — Mathlib

English

If ContDiffOn ω f s, then ContDiffOn on s within any neighborhood u of each point.

Русский

Если ContDiffOn ω f s, тогда ContDiffOn на s внутри окрестности каждого x.

LaTeX

$$$\text{ContDiffOn } 𝕜 ω f s \Rightarrow \forall x\in s, \exists u\ni x: \ContDiffOn 𝕜 ω f (s\cap u)$$$

Lean4

theorem contDiffOn (hm : m ≤ n) (h' : m = ∞ → n = ω) (h : ContDiffWithinAt 𝕜 n f s x) :
    ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u :=
  by
  obtain ⟨_u, uo, xu, h⟩ := h.contDiffOn' hm h'
  exact ⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩

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