Theorems · Definition · functional analysis

SchwartzMap.seminorm

(𝕜 : Type u_2) →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [inst_4 : NormedField 𝕜] →
                [inst_5 : NormedSpace 𝕜 F] → [inst_6 : SMulCommClass ℝ 𝕜 F] → ℕ → ℕ → Seminorm 𝕜 (SchwartzMap E F)

The seminorms of the Schwartz space given by the best constants in the definition of 𝓢(E, F).

Defined in

Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Cited by

16 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedFieldNormedSpaceSMulCommClass