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