norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin

English

The operator norm of the iterated Fréchet derivative equals the norm of the corresponding iterated derivative.

Русский

Нормa оператора итеративной ФрÉше-производной равна норме соответствующей итеративной производной.

LaTeX

$$$ ‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖ $$$

Lean4

theorem norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin :
    ‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖ := by
  rw [iteratedDerivWithin_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]

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