iteratedDerivWithin_eq_iteratedFDerivWithin

English

The iterated derivative within s equals the iterated Fréchet derivative within s when expressed via the iterated Fréchet derivative map.

Русский

Итеративная производная внутри s равна итеративной производной Фрéше внутри s, когда она выражена через отображение итеративной Фрéше-производной.

LaTeX

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

Lean4

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

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