ι : Type u_4
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_1
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
⊢ Function.Surjective ↑(OrthogonalFamily.linearIsometry hVortho).toLinearMap
ι : Type u_4
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_1
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
⊢ Function.Surjective ↑(OrthogonalFamily.linearIsometry hVortho)
rw [← LinearIsometry.coe_toLinearMap]
no goals
ι : Type u_4
𝕜 : Type u_2
inst✝⁵ : IsROrC 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_1
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
⊢ Function.Surjective ↑(OrthogonalFamily.linearIsometry hVortho).toLinearMap
exact LinearMap.range_eq_top.mp
  (eq_top_iff.mpr <| hVtotal.trans_eq hVortho.range_linearIsometry.symm)