English
For any ENat n, ContDiff 𝕜 n f is equivalent to HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f).
Русский
Для любого ENat n ContDiff 𝕜 n f эквивалентно HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f).
LaTeX
$$$\operatorname{ContDiff}_{\mathbb{K}}\ n\ f \iff \operatorname{HasFTaylorSeriesUpTo}\ n\ f\ (ftaylorSeries\ 𝕜\ f)$$$
Lean4
/-- When a function is `C^n`, it admits `ftaylorSeries 𝕜 f` as a Taylor series up
to order `n` in `s`. -/
theorem ftaylorSeries (hf : ContDiff 𝕜 n f) : HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f) :=
by
simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ] at hf ⊢
exact ContDiffOn.ftaylorSeriesWithin hf uniqueDiffOn_univ