English
The canonical ring (or additive) equivalence lpBCF maps lp-based objects to bounded continuous functions by evaluation.
Русский
Каноническое отображение lpBCF переводит lp-объекты в ограниченные непрерывные функции по значению.
LaTeX
$$lpBCF$$
Lean4
/-- The canonical map between `lp (fun _ : α ↦ A) ∞` and `α →ᵇ A` as an `AlgEquiv`. -/
noncomputable def lpBCF : lp (fun _ : α ↦ A) ∞ ≃ₐ[𝕜] α →ᵇ A :=
{ RingEquiv.lpBCF A with commutes' := fun _k ↦ rfl }