Theorems · Definition · functional analysis

ContDiffMapSupportedIn.mkCLMtoNormedSpace

(𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    {n : ℕ∞} →
                      {K : TopologicalSpace.Compacts E} →
                        {G : Type u_5} →
                          [inst_7 : NormedAddCommGroup G] →
                            [inst_8 : NormedSpace 𝕜 G] →
                              (A : ContDiffMapSupportedIn E F n K → G) →
                                (∀ (f g : ContDiffMapSupportedIn E F n K), A (f + g) = A f + A g) →
                                  (∀ (c : 𝕜) (f : ContDiffMapSupportedIn E F n K), A (c • f) = c • A f) →
                                    (∃ s C,
                                        0 ≤ C ∧
                                          ∀ (f : ContDiffMapSupportedIn E F n K),
                                            ‖A f‖ ≤
                                              C * (s.sup fun i => ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f) →
                                      ContDiffMapSupportedIn E F n K →L[𝕜] G

Define a continous 𝕜-linear map fom 𝓓^{n}_{K}(E, F) to a normed space.

Defined in

Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpaceSMulCommClassNormedAddCommGroupNormedSpace