iteratedFDerivWithin_univ — Mathlib

English

The iterated derivative within the whole space is the same as the global iterated derivative.

Русский

Итеративная производная внутри пространства равна глобальной итеративной производной.

LaTeX

$$$\operatorname{iteratedFDerivWithin}_{\mathbb{k}} \; n\; f\; \mathrm{univ} = \operatorname{iteratedFDeriv}_{\mathbb{k}} \; n\; f$$$

Lean4

theorem iteratedFDerivWithin_univ {n : ℕ} : iteratedFDerivWithin 𝕜 n f univ = iteratedFDeriv 𝕜 n f := by
  induction n with
  | zero => ext x; simp
  | succ n IH =>
    ext x m
    rw [iteratedFDeriv_succ_apply_left, iteratedFDerivWithin_succ_apply_left, IH, fderivWithin_univ]

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