deriv — Mathlib

English

If a function f: 𝕜 → E has compact support, then its derivative has compact support as well.

Русский

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

LaTeX

$$$\\text{HasCompactSupport}(f) \\Rightarrow \\text{HasCompactSupport}(\\operatorname{deriv} f)$$$

Lean4

protected theorem deriv (hf : HasCompactSupport f) : HasCompactSupport (deriv f) :=
  hf.mono' support_deriv_subset

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