case refine'_1
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap ≤
    topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)

case refine'_2
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap) ≤
    LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap =
    topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
refine' le_antisymm _ _
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
⊢ ↑(OrthogonalFamily.linearIsometry hV).toLinearMap f ∈
    topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
case refine'_1
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap ≤
    topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
rintro x ⟨f, rfl⟩
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
⊢ ∀ (x : Finset ι), ∑ b in x, (fun i => ↑(V i) (↑f i)) b ∈ ↑(⨆ (i : ι), LinearMap.range (V i).toLinearMap)
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
⊢ ↑(OrthogonalFamily.linearIsometry hV).toLinearMap f ∈
    topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap)
refine' mem_closure_of_tendsto (hV.hasSum_linearIsometry f) (eventually_of_forall _)
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
⊢ ∑ b in s, (fun i => ↑(V i) (↑f i)) b ∈ ↑(⨆ (i : ι), LinearMap.range (V i).toLinearMap)
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
⊢ ∀ (x : Finset ι), ∑ b in x, (fun i => ↑(V i) (↑f i)) b ∈ ↑(⨆ (i : ι), LinearMap.range (V i).toLinearMap)
intro s
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
⊢ ∑ b in s, (fun i => ↑(V i) (↑f i)) b ∈ ⨆ (i : ι), LinearMap.range (V i).toLinearMap
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
⊢ ∑ b in s, (fun i => ↑(V i) (↑f i)) b ∈ ↑(⨆ (i : ι), LinearMap.range (V i).toLinearMap)
rw [SetLike.mem_coe]
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
⊢ ∀ (c : ι), c ∈ s → (fun i => ↑(V i) (↑f i)) c ∈ ⨆ (i : ι), LinearMap.range (V i).toLinearMap
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
⊢ ∑ b in s, (fun i => ↑(V i) (↑f i)) b ∈ ⨆ (i : ι), LinearMap.range (V i).toLinearMap
refine' sum_mem _
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
i : ι
a✝ : i ∈ s
⊢ (fun i => ↑(V i) (↑f i)) i ∈ ⨆ (i : ι), LinearMap.range (V i).toLinearMap
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
⊢ ∀ (c : ι), c ∈ s → (fun i => ↑(V i) (↑f i)) c ∈ ⨆ (i : ι), LinearMap.range (V i).toLinearMap
intro i _
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
i : ι
a✝ : i ∈ s
⊢ (fun i => ↑(V i) (↑f i)) i ∈ LinearMap.range (V i).toLinearMap
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
i : ι
a✝ : i ∈ s
⊢ (fun i => ↑(V i) (↑f i)) i ∈ ⨆ (i : ι), LinearMap.range (V i).toLinearMap
refine' mem_iSup_of_mem i _
no goals
case refine'_1.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : { x // x ∈ lp G 2 }
s : Finset ι
i : ι
a✝ : i ∈ s
⊢ (fun i => ↑(V i) (↑f i)) i ∈ LinearMap.range (V i).toLinearMap
exact LinearMap.mem_range_self _ (f i)
case refine'_2.h
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ (⨆ (i : ι), LinearMap.range (V i).toLinearMap) ≤ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap

case refine'_2.ht
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ IsClosed ↑(LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap)
case refine'_2
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ topologicalClosure (⨆ (i : ι), LinearMap.range (V i).toLinearMap) ≤
    LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
apply topologicalClosure_minimal
no goals
case refine'_2.ht
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ IsClosed ↑(LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap)
exact hV.linearIsometry.isometry.uniformInducing.isComplete_range.isClosed
case refine'_2.h
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ ∀ (i : ι), LinearMap.range (V i).toLinearMap ≤ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
case refine'_2.h
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ (⨆ (i : ι), LinearMap.range (V i).toLinearMap) ≤ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
refine' iSup_le _
case refine'_2.h.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
i : ι
x : G i
⊢ ↑(V i).toLinearMap x ∈ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
case refine'_2.h
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ ∀ (i : ι), LinearMap.range (V i).toLinearMap ≤ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
rintro i x ⟨x, rfl⟩
case refine'_2.h.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
i : ι
x : G i
⊢ ↑(OrthogonalFamily.linearIsometry hV).toLinearMap (lp.single 2 i x) = ↑(V i).toLinearMap x
case refine'_2.h.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
i : ι
x : G i
⊢ ↑(V i).toLinearMap x ∈ LinearMap.range (OrthogonalFamily.linearIsometry hV).toLinearMap
use lp.single 2 i x
no goals
case refine'_2.h.intro
ι : Type u_4
𝕜 : Type u_3
inst✝⁵ : IsROrC 𝕜
E : Type u_2
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
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
i : ι
x : G i
⊢ ↑(OrthogonalFamily.linearIsometry hV).toLinearMap (lp.single 2 i x) = ↑(V i).toLinearMap x
exact hV.linearIsometry_apply_single x