iteratedFDeriv — Mathlib

English

If f has compact support, then its iterated derivatives also have compact support.

Русский

Если функция f имеет компактную опору, то её повторные производные также имеют компактную опору.

LaTeX

$$$\text{HasCompactSupport}(f) \Rightarrow \forall n,\ \text{HasCompactSupport}(\operatorname{iteratedFDeriv}_{\mathbb{k}}\; n\; f)$$$

Lean4

theorem iteratedFDeriv (hf : HasCompactSupport f) (n : ℕ) : HasCompactSupport (iteratedFDeriv 𝕜 n f) :=
  hf.of_isClosed_subset isClosed_closure (tsupport_iteratedFDeriv_subset n)

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