𝕜 : Type u_3
E : Type u_1
F : Type ?u.871455
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : CompleteSpace E
ι : Type u_2
inst✝¹ : SemilatticeSup ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), CompleteSpace { x // x ∈ U t }
hU : Monotone U
x : E
hU' : Submodule.topologicalClosure (⨆ (t : ι), U t) = ⊤
⊢ Tendsto (fun t => ↑(↑(orthogonalProjection (U t)) x)) atTop (𝓝 x)
𝕜 : Type u_3
E : Type u_1
F : Type ?u.871455
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : CompleteSpace E
ι : Type u_2
inst✝¹ : SemilatticeSup ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), CompleteSpace { x // x ∈ U t }
hU : Monotone U
x : E
hU' : ⊤ ≤ Submodule.topologicalClosure (⨆ (t : ι), U t)
⊢ Tendsto (fun t => ↑(↑(orthogonalProjection (U t)) x)) atTop (𝓝 x)
rw [← eq_top_iff] at hU'
case h.e'_5.h.e'_3
𝕜 : Type u_3
E : Type u_1
F : Type ?u.871455
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : CompleteSpace E
ι : Type u_2
inst✝¹ : SemilatticeSup ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), CompleteSpace { x // x ∈ U t }
hU : Monotone U
x : E
hU' : Submodule.topologicalClosure (⨆ (t : ι), U t) = ⊤
⊢ x = ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
𝕜 : Type u_3
E : Type u_1
F : Type ?u.871455
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : CompleteSpace E
ι : Type u_2
inst✝¹ : SemilatticeSup ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), CompleteSpace { x // x ∈ U t }
hU : Monotone U
x : E
hU' : Submodule.topologicalClosure (⨆ (t : ι), U t) = ⊤
⊢ Tendsto (fun t => ↑(↑(orthogonalProjection (U t)) x)) atTop (𝓝 x)
convert orthogonalProjection_tendsto_closure_iSup U hU x
𝕜 : Type u_3
E : Type u_1
F : Type ?u.871455
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : CompleteSpace E
ι : Type u_2
inst✝¹ : SemilatticeSup ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), CompleteSpace { x // x ∈ U t }
hU : Monotone U
x : E
hU' : Submodule.topologicalClosure (⨆ (t : ι), U t) = ⊤
⊢ x ∈ Submodule.topologicalClosure (⨆ (i : ι), U i)
case h.e'_5.h.e'_3
𝕜 : Type u_3
E : Type u_1
F : Type ?u.871455
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : CompleteSpace E
ι : Type u_2
inst✝¹ : SemilatticeSup ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), CompleteSpace { x // x ∈ U t }
hU : Monotone U
x : E
hU' : Submodule.topologicalClosure (⨆ (t : ι), U t) = ⊤
⊢ x = ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
rw [orthogonalProjection_eq_self_iff.mpr _]
𝕜 : Type u_3
E : Type u_1
F : Type ?u.871455
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : CompleteSpace E
ι : Type u_2
inst✝¹ : SemilatticeSup ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), CompleteSpace { x // x ∈ U t }
hU : Monotone U
x : E
hU' : Submodule.topologicalClosure (⨆ (t : ι), U t) = ⊤
⊢ x ∈ ⊤
𝕜 : Type u_3
E : Type u_1
F : Type ?u.871455
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : CompleteSpace E
ι : Type u_2
inst✝¹ : SemilatticeSup ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), CompleteSpace { x // x ∈ U t }
hU : Monotone U
x : E
hU' : Submodule.topologicalClosure (⨆ (t : ι), U t) = ⊤
⊢ x ∈ Submodule.topologicalClosure (⨆ (i : ι), U i)
rw [hU']
no goals
𝕜 : Type u_3
E : Type u_1
F : Type ?u.871455
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝² : CompleteSpace E
ι : Type u_2
inst✝¹ : SemilatticeSup ι
U : ι → Submodule 𝕜 E
inst✝ : ∀ (t : ι), CompleteSpace { x // x ∈ U t }
hU : Monotone U
x : E
hU' : Submodule.topologicalClosure (⨆ (t : ι), U t) = ⊤
⊢ x ∈ ⊤
trivial