continuous_fderiv — Mathlib

English

If HasFTaylorSeriesUpToOn n f p s and for every m the derivatives agree on s with q, then HasFTaylorSeriesUpToOn n f q s.

Русский

Если есть разложение HasFTaylorSeriesUpToOn n f p s и для каждого m производные совпадают на s с q, то HasFTaylorSeriesUpToOn n f q s.

LaTeX

$$$HasFTaylorSeriesUpToOn\ n\ f\ p\ s \to (\forall m, le\ (m) n) \to (\forall x \in s, p x m = q x m) \to HasFTaylorSeriesUpToOn n f q s$$$

Lean4

theorem continuous_fderiv (h : ContDiff 𝕜 n f) (hn : 1 ≤ n) : Continuous (fderiv 𝕜 f) :=
  (contDiff_one_iff_fderiv.1 (h.of_le hn)).2

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