equivₗᵢ — Mathlib

English

There is a canonical linear isometric equivalence between the Lp space with p = ∞, over a family β_i, and the product space ∀ i, β_i.

Русский

Существует каноническое линейно изометрическое эквивелентное отображение между пространством L^∞ над семейством β_i и произведением объектов β_i по всем i.

LaTeX

$$$\PiLp_∞(β) \;\cong_{\text{LinIso}}\; \prod_{i} β_i$$$

Lean4

/-- The canonical map `WithLp.equiv` between `PiLp ∞ β` and `Π i, β i` as a linear isometric
equivalence. -/
def equivₗᵢ : PiLp ∞ β ≃ₗᵢ[𝕜] (∀ i, β i) where
  __ := WithLp.linearEquiv p 𝕜 _
  norm_map' := norm_ofLp

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