case h.e'_4.h.e'_9
ι : Type u_3
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.653291
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
⊢ (⨆ (i : ι), LinearMap.range (LinearIsometry.toSpanSingleton 𝕜 E (_ : ‖v i‖ = 1)).toLinearMap) = span 𝕜 (Set.range v)
ι : Type u_3
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.653291
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
⊢ ⊤ ≤ topologicalClosure (⨆ (i : ι), LinearMap.range (LinearIsometry.toSpanSingleton 𝕜 E (_ : ‖v i‖ = 1)).toLinearMap)
convert hsp
no goals
case h.e'_4.h.e'_9
ι : Type u_3
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.653291
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
F : ι → Submodule 𝕜 E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ topologicalClosure (span 𝕜 (Set.range v))
⊢ (⨆ (i : ι), LinearMap.range (LinearIsometry.toSpanSingleton 𝕜 E (_ : ‖v i‖ = 1)).toLinearMap) = span 𝕜 (Set.range v)
simp [← LinearMap.span_singleton_eq_range, ← Submodule.span_iUnion]