Theorems · Definition · general topology

ContinuousMap.linearIsometryBoundedOfCompact

(α : Type u_1) →
  (E : Type u_3) →
    [inst : TopologicalSpace α] →
      [inst_1 : CompactSpace α] →
        [inst_2 : SeminormedAddCommGroup E] →
          (𝕜 : Type u_4) →
            [inst_3 : NormedRing 𝕜] →
              [inst_4 : Module 𝕜 E] → [inst_5 : IsBoundedSMul 𝕜 E] → C(α, E) ≃ₗᵢ[𝕜] BoundedContinuousFunction α E

When α is compact and 𝕜 is a normed field, the 𝕜-algebra of bounded continuous maps α →ᵇ β is 𝕜-linearly isometric to C(α, β).

Defined in

Mathlib.Topology.ContinuousMap.Compact

Cited by

10 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCompactSpaceSeminormedAddCommGroupNormedRingModuleIsBoundedSMul