Theorems · Definition · functional analysis

BoundedContinuousFunction.compContinuousCLM

{α : Type u} →
  (β : Type v) →
    {γ : Type w} →
      [inst : TopologicalSpace α] →
        [inst_1 : SeminormedAddCommGroup β] →
          (𝕜 : Type u_2) →
            [inst_2 : TopologicalSpace γ] →
              [inst_3 : NormedField 𝕜] →
                [inst_4 : NormedSpace 𝕜 β] → C(γ, α) → BoundedContinuousFunction α β →L[𝕜] BoundedContinuousFunction γ β

Precomposition with a continuous map is a continuous linear map from bounded continuous functions to bounded continuous functions.

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Normed

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSeminormedAddCommGroupTopologicalSpaceNormedFieldNormedSpace