support_iteratedFDeriv_subset — Mathlib

English

For every n, the support of the n-th iterated Fréchet derivative of f is contained in the topological support of f.

Русский

Для каждого n опора n-й повторной производной Фрéше равна подмножеству топологической опоры функции f.

LaTeX

$$$\operatorname{supp}(\operatorname{iteratedFDeriv}_{\mathbb{k}}\; n\; f) \subseteq \operatorname{tsupport}(f)$$$

Lean4

theorem support_iteratedFDeriv_subset (n : ℕ) : support (iteratedFDeriv 𝕜 n f) ⊆ tsupport f :=
  subset_closure.trans (tsupport_iteratedFDeriv_subset n)

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