Theorems · Inductive type · functional analysis

ContDiffMapSupportedIn

(E : Type u_2) →
  (F : Type u_3) →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [NormedSpace ℝ F] → ℕ∞ → TopologicalSpace.Compacts E → Type (max u_2 u_3)

The type of bundled n-times continuously differentiable maps which vanish outside of a fixed compact set K.

Defined in

Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Cited by

107 results in Mathlib

Foundations

Depth 157 from the axioms, rests on 3,652 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace