Support of the derivative of a function

In this file we prove that the (topological) support of a function includes the support of its derivative. As a corollary, we show that the derivative of a function with compact support has compact support.

Keywords

derivative, support

Support of derivatives

theorem support_deriv_subset {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} : Function.support (deriv f) ⊆ tsupport f

theorem HasCompactSupport.deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : HasCompactSupport f) : HasCompactSupport (deriv f)