lpBCFₗᵢ — Mathlib

English

The canonical map between lp E p and PiLp p E for finite α is defined by the identity on functions and by inclusion into the product space.

Русский

Каноническое отображение между lp E p и PiLp p E для конечного α определяется единично на функциях и включением в произведение.

LaTeX

$$lpPiLp Def$$

Lean4

/-- The canonical map between `lp (fun _ : α ↦ E) ∞` and `α →ᵇ E` as a `LinearIsometryEquiv`. -/
noncomputable def lpBCFₗᵢ : lp (fun _ : α ↦ E) ∞ ≃ₗᵢ[𝕜] α →ᵇ E :=
  { AddEquiv.lpBCF with
    map_smul' := fun _ _ ↦ rfl
    norm_map' := fun f ↦ by simp only [norm_eq_iSup_norm, lp.norm_eq_ciSup]; rfl }

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