iteratedFDeriv_right' — Mathlib

English

A version stating that x ↦ iteratedFDeriv_right is ContDiff if f is ContDiff with higher order.

Русский

Версия, говорящая, что x ↦ iteratedFDeriv_right гладко, если f гладко в более высоком порядке.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}} n f \Rightarrow \operatorname{ContDiff}_{\mathbb{K}} (n) (\text{iteratedFDeriv_right } i f)$$$

Lean4

@[fun_prop]
theorem iteratedFDeriv_right' {i : ℕ} (hf : ContDiff 𝕜 (m + i) f) : ContDiff 𝕜 m (iteratedFDeriv 𝕜 i f) :=
  contDiff_iff_contDiffAt.mpr fun _x => hf.contDiffAt.iteratedFDeriv_right (le_refl _)

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