piLIE — Mathlib

English

There is a natural linear isometry between families of maps and maps into the product space, a PiLIE correspondence.

Русский

Существует естественная линейная изометрия между семействами отображений и отображениями в произведение пространств (PiLIE соответствие).

LaTeX

$$$\mathrm{piLIE} : (\forall i', E [⋀^ι]→L[𝕜] F i') \simeq_{ℓ} (E [⋀^ι]→L[𝕜] (\forall i, F i))$$$

Lean4

/-- `ContinuousAlternatingMap.pi` as a `LinearIsometryEquiv`. -/
@[simps!]
def piLIE {ι' : Type*} [Fintype ι'] {F : ι' → Type*} [∀ i', SeminormedAddCommGroup (F i')]
    [∀ i', NormedSpace 𝕜 (F i')] : (∀ i', E [⋀^ι]→L[𝕜] F i') ≃ₗᵢ[𝕜] (E [⋀^ι]→L[𝕜] (∀ i, F i))
    where
  toLinearEquiv := piLinearEquiv
  norm_map' := opNorm_pi

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