iteratedDerivWithin_univ — Mathlib

English

The iterated derivative within s equals the iterated Fréchet derivative within s, expressed as a composition with the appropriate equivalence.

Русский

Итеративная производная внутри s равна итеративной Фрéше-производной внутри s, представленная через соответствующее эквивалентное отображение.

LaTeX

$$$ iteratedDerivWithin n f s = (iteratedFDerivWithin 𝕜 n f s x : (Fin n → 𝕜) → F) fun _ : Fin n => 1 $$$

Lean4

theorem iteratedDerivWithin_univ : iteratedDerivWithin n f univ = iteratedDeriv n f :=
  by
  ext x
  rw [iteratedDerivWithin, iteratedDeriv, iteratedFDerivWithin_univ]

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