# 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)
: