contDiffOn_of_locally_contDiffOn — Mathlib

English

See above

Русский

См. выше

LaTeX

$$$ContDiffOn\\ 𝕜\\ (n+1)\\ f\\ s\\ \\leftrightarrow\\ \\forall x\\in s,\\exists u\\in\\mathcal{N}[insert x s] x,\\,(n=\\omega\\to AnalyticOn\\ 𝕜 f\\ u)\\land \\exists f' : E\\to E \\toL[\\mathbb{𝕜}] F,\\ (\\forall x\\in u, HasFDerivWithinAt f (f' x) u x)\\land ContDiffOn\\ 𝕜 n\\ f'\\ u$$$

Lean4

/-- If a function is `C^n` around each point in a set, then it is `C^n` on the set. -/
theorem contDiffOn_of_locally_contDiffOn (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)) :
    ContDiffOn 𝕜 n f s := by
  intro x xs
  rcases h x xs with ⟨u, u_open, xu, hu⟩
  apply (contDiffWithinAt_inter _).1 (hu x ⟨xs, xu⟩)
  exact IsOpen.mem_nhds u_open xu

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