English
If f has a Taylor series up to n, then f is ContDiff of order n.
Русский
Если у функции f есть ряд Тейлора до n, то f является ContDiff порядка n.
LaTeX
$$$HasFTaylorSeriesUpTo\ n\ f\ f'\Rightarrow ContDiff\ 𝕜\ n\ f$$$
Lean4
/-- A function is continuously differentiable up to `n` if it admits derivatives up to
order `n`, which are continuous. Contrary to the case of definitions in domains (where derivatives
might not be unique) we do not need to localize the definition in space or time.
-/
@[fun_prop]
def ContDiff (n : WithTop ℕ∞) (f : E → F) : Prop :=
match n with
| ω => ∃ p : E → FormalMultilinearSeries 𝕜 E F, HasFTaylorSeriesUpTo ⊤ f p ∧ ∀ i, AnalyticOnNhd 𝕜 (fun x ↦ p x i) univ
| (n : ℕ∞) => ∃ p : E → FormalMultilinearSeries 𝕜 E F, HasFTaylorSeriesUpTo n f p
