Support of the derivative of a function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : 𝕜 → E} :
function.support (deriv f) ⊆ tsupport f
theorem
has_compact_support.deriv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type v}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : 𝕜 → E}
(hf : has_compact_support f) :