lpBCF — Mathlib

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 }

Похожие утверждения