Theorems · Definition · functional analysis

ContDiffMapSupportedIn.of_support_subset

{E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} →
              {K : TopologicalSpace.Compacts E} →
                {f : E → F} → ContDiff ℝ (↑n) f → Function.support f ⊆ ↑K → ContDiffMapSupportedIn E F n K

Inclusion of unbundled n-times continuously differentiable function with support included in a compact K into the space 𝓓^{n}_{K}.

Defined in

Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Cited by

5 results in Mathlib

Foundations

Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace