continuous_iteratedFDeriv — Mathlib

English

Same as above, but specialized version with a Prop attribute for the continuous iterated derivative.

Русский

То же самое, специализированная версия с пометкой о непрерывности.

LaTeX

$$$\,[fun_prop]\totheorem\ Continious\ iteratedFDeriv'\ (hf:\operatorname{ContDiff}\ 𝕜 m f)\Rightarrow \text{Continuous}(x\mapsto \operatorname{iteratedFDeriv}_{\mathbb{K}}\ m f x)$$$

Lean4

/-- If `f` is `C^n` then its `m`-times iterated derivative is continuous for `m ≤ n`. -/
theorem continuous_iteratedFDeriv {m : ℕ} (hm : m ≤ n) (hf : ContDiff 𝕜 n f) :
    Continuous fun x => iteratedFDeriv 𝕜 m f x :=
  (contDiff_iff_continuous_differentiable.mp (hf.of_le hm)).1 m le_rfl

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