English
The range of the canonical linear isometry is the closure of the join of the ranges of the V_i's.
Русский
Объем линейной изометрии равен замыканию объединения диапазонов V_i.
LaTeX
$$$ \\mathrm{range}\\big( hV.linearIsometry \\big) = \\overline{\\big\\( \\bigvee_i \\mathrm{range}(V_i) \\big\\!\\big)}$$$
Lean4
/-- If `V : Π i, G i →ₗᵢ[𝕜] E` is an orthogonal family such that the supremum of the ranges of
`V i` is dense, then `(E, V)` is a Hilbert sum of `G`. -/
theorem mk [∀ i, CompleteSpace <| G i] (hVortho : OrthogonalFamily 𝕜 G V)
(hVtotal : ⊤ ≤ (⨆ i, LinearMap.range (V i).toLinearMap).topologicalClosure) : IsHilbertSum 𝕜 G V :=
{ OrthogonalFamily := hVortho
surjective_isometry := by
rw [← LinearIsometry.coe_toLinearMap]
exact LinearMap.range_eq_top.mp (eq_top_iff.mpr <| hVtotal.trans_eq hVortho.range_linearIsometry.symm) }
