Theorems · Definition · functional analysis

AlgEquiv.lpBCF

(α : Type u_1) →
  {A : Type u_4} →
    (𝕜 : Type u_5) →
      [inst : TopologicalSpace α] →
        [DiscreteTopology α] →
          [inst_2 : NormedRing A] →
            [inst_3 : NormOneClass A] →
              [inst_4 : NontriviallyNormedField 𝕜] →
                [inst_5 : NormedAlgebra 𝕜 A] → ↥(lp (fun x => A) ⊤) ≃ₐ[𝕜] BoundedContinuousFunction α A

The canonical map between lp (fun _ : α ↦ A) ∞ and α →ᵇ A as an AlgEquiv.

Defined in

Mathlib.Analysis.Normed.Lp.LpEquiv

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDiscreteTopologyNormedRingNormOneClassNontriviallyNormedFieldNormedAlgebra