contDiffOn — Mathlib

English

If HasFTaylorSeriesUpToOn holds for n on s with function f, then f is ContDiffOn on s.

Русский

Если существует разложение Фолмала F Taylor до на множество s для f, то f является ContDiffOn на s.

LaTeX

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

Lean4

theorem contDiffOn {n : ℕ∞} {f' : E → FormalMultilinearSeries 𝕜 E F} (hf : HasFTaylorSeriesUpToOn n f f' s) :
    ContDiffOn 𝕜 n f s := by
  intro x hx m hm
  use s
  simp only [Set.insert_eq_of_mem hx, self_mem_nhdsWithin, true_and]
  exact ⟨f', hf.of_le (mod_cast hm)⟩

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