RellichKondrachov.Analysis.Calculus.ContDiff.Support #
Small glue lemmas relating ContDiffOn to ContDiff using topological support.
The key pattern is: if f is C^n on an open set s and the topological support tsupport f
is contained in s, then f is globally C^n (it is 0 in a neighborhood of every point
outside s).
theorem
RellichKondrachov.Analysis.Calculus.ContDiff.contDiff_of_contDiffOn_of_tsupport_subset
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{f : E → F}
{s : Set E}
(hs : IsOpen s)
(hf : ContDiffOn 𝕜 n f s)
(hSupp : tsupport f ⊆ s)
:
ContDiff 𝕜 n f
If f is C^n on an open set s and tsupport f ⊆ s, then f is globally C^n.