English
The operator prodₗᵢ is the canonical linear isometry equivalence between the product of two operator spaces and the operator space of the product: (E→L M1 M2) × (E→L M3 M4) ≃ᶦR E→L (M2 × M4).
Русский
Операция prodₗᵢ является каноническим линейным изометрическим эквивалентом между произведением двух пространств ограниченных линейных отображений и пространством линейных отображений в произведение:
LaTeX
$$$$ (E \\to_L M_1) \\times (E \\to_L M_3) \\; \\cong_{\,\\mathrm{isom}} \\; E \\to_L (M_1 \\times M_3). $$$$
Lean4
/-- The injection `x ↦ Pi.single i x` as a linear isometry. -/
protected def single [∀ i, SeminormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (i : ι) : E i →ₗᵢ[𝕜] Π j, E j :=
(LinearMap.single 𝕜 E i).toLinearIsometry (.single i)
