English
In the canonical isometric isomorphism, the symmetrized inverse applied to a finitely-supported combination corresponds to the finite sum of images.
Русский
В каноническом изометрическом изоморфизме обратное отображение на ограниченной по поддержке сумме соответствует конечной сумме образов.
LaTeX
$$$ h_V.linearIsometryEquiv.symm (W_0.Sum(\\ell^2) (\\lambda i, G_i)) = W_0.\\sum_i V_i $$$
Lean4
/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
`lp G 2`, an "elementary basis vector" in `lp G 2` supported at `i : ι` is the image of the
associated element in `E`. -/
@[simp]
protected theorem linearIsometryEquiv_symm_apply_single [DecidableEq ι] (hV : IsHilbertSum 𝕜 G V) {i : ι} (x : G i) :
hV.linearIsometryEquiv.symm (lp.single 2 i x) = V i x := by
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply_single]
