Theorems · Definition · functional analysis

AddEquiv.lpBCF

{α : Type u_1} →
  {E : Type u_2} →
    [inst : TopologicalSpace α] →
      [DiscreteTopology α] → [inst_2 : NormedAddCommGroup E] → ↥(lp (fun x => E) ⊤) ≃+ BoundedContinuousFunction α E

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

Defined in

Mathlib.Analysis.Normed.Lp.LpEquiv

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDiscreteTopologyNormedAddCommGroup