norm_iteratedFDeriv_zero — Mathlib

English

The tsupport of iteratedFDeriv 𝕜 n f is contained in the tsupport of f for all n.

Русский

Опорная поддержка итеративной производной ограничена опорой самой функции.

LaTeX

$$$\operatorname{tsupport}(\operatorname{iteratedFDeriv}_{\mathbb{K}}^{n} f) \subseteq \operatorname{tsupport}(f)$$$

Lean4

@[simp]
theorem norm_iteratedFDeriv_zero : ‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖ := by
  rw [iteratedFDeriv_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]

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