English
There exists a canonical LinearIsometryEquiv between lp E p and PiLp p E under finite index and 1 ≤ p; it preserves linear structure and norms.
Русский
Существует каноническое линейноизометрическое эквив between lp E p и PiLp p E при конечном индексе и 1 ≤ p; сохраняет линейную структуру и нормы.
LaTeX
$$$lp E p \cong_{lin} PiLp p E$$$
Lean4
/-- The canonical `LinearIsometryEquiv` between `lp E p` and `PiLp p E` when `E : α → Type u`
with `[Fintype α]` and `[Fact (1 ≤ p)]`. -/
noncomputable def lpPiLpₗᵢ [Fact (1 ≤ p)] : lp E p ≃ₗᵢ[𝕜] PiLp p E :=
{ AddEquiv.lpPiLp with
map_smul' := fun _k _f ↦ rfl
norm_map' := equiv_lpPiLp_norm }
