contDiffWithinAt_iff_contDiffOn_nhds

English

Given HasFTaylorSeriesUpToOn, f is ContDiffOn on s.

Русский

При наличии HasFTaylorSeriesUpToOn функция f гладкая в s.

LaTeX

$$$\text{HasFTaylorSeriesUpToOn } n\; f\; s \Rightarrow \text{ContDiffOn } 𝕜 n f s$$$

Lean4

/-- A function is `C^n` within a set at a point, for `n : ℕ`, if and only if it is `C^n` on
a neighborhood of this point. -/
theorem contDiffWithinAt_iff_contDiffOn_nhds (hn : n ≠ ∞) :
    ContDiffWithinAt 𝕜 n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContDiffOn 𝕜 n f u :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases h.contDiffOn le_rfl (by simp [hn]) with ⟨u, hu, h'u⟩
    exact ⟨u, hu, h'u.2⟩
  · rcases h with ⟨u, u_mem, hu⟩
    have : x ∈ u := mem_of_mem_nhdsWithin (mem_insert x s) u_mem
    exact (hu x this).mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert x s) u_mem)

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