case inl
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : IsEmpty ι
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))

case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
cases isEmpty_or_nonempty ι
case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
let y := (orthogonalProjection (⨆ i, U i).topologicalClosure x : E)
case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
have proj_x : ∀ i, orthogonalProjection (U i) x = orthogonalProjection (U i) y := fun i =>
  (orthogonalProjection_orthogonalProjection_of_le
      ((le_iSup U i).trans (iSup U).le_topologicalClosure) _).symm
case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
⊢ ∀ (ε : ℝ), ε > 0 → ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
suffices ∀ ε > 0, ∃ I, ∀ i ≥ I, ‖(orthogonalProjection (U i) y : E) - y‖ < ε by
  simpa only [proj_x, NormedAddCommGroup.tendsto_atTop] using this
case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
⊢ ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
⊢ ∀ (ε : ℝ), ε > 0 → ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
intro ε hε
case inr.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : dist y a < ε
⊢ ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
case inr
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
⊢ ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
obtain ⟨a, ha, hay⟩ : ∃ a ∈ ⨆ i, U i, dist y a < ε := by
  have y_mem : y ∈ (⨆ i, U i).topologicalClosure := Submodule.coe_mem _
  rw [← SetLike.mem_coe, Submodule.topologicalClosure_coe, Metric.mem_closure_iff] at y_mem
  exact y_mem ε hε
case inr.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
⊢ ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
case inr.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : dist y a < ε
⊢ ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
rw [dist_eq_norm] at hay
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
⊢ ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
case inr.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
⊢ ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
obtain ⟨I, hI⟩ : ∃ I, a ∈ U I := by rwa [Submodule.mem_iSup_of_directed _ hU.directed_le] at ha
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
⊢ ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
refine' ⟨I, fun i (hi : I ≤ i) => _⟩
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ (⨅ (x : { x // x ∈ U i }), ‖y - ↑x‖) < ε
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
rw [norm_sub_rev, orthogonalProjection_minimal]
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ (⨅ (x : { x // x ∈ U i }), ‖y - ↑x‖) ≤ ‖y - a‖
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ (⨅ (x : { x // x ∈ U i }), ‖y - ↑x‖) < ε
refine' lt_of_le_of_lt _ hay
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ (⨅ (x : { x // x ∈ U i }), ‖y - ↑x‖) ≤ ‖y - ↑{ val := a, property := (_ : a ∈ U i) }‖
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ (⨅ (x : { x // x ∈ U i }), ‖y - ↑x‖) ≤ ‖y - a‖
change _ ≤ ‖y - (⟨a, hU hi hI⟩ : U i)‖
no goals
case inr.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ (⨅ (x : { x // x ∈ U i }), ‖y - ↑x‖) ≤ ‖y - ↑{ val := a, property := (_ : a ∈ U i) }‖
exact ciInf_le ⟨0, Set.forall_range_iff.mpr fun _ => norm_nonneg _⟩ _
case inl
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : IsEmpty ι
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) ⊥
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
case inl
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : IsEmpty ι
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
rw [filter_eq_bot_of_isEmpty (atTop : Filter ι)]
no goals
case inl
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : IsEmpty ι
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) ⊥
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
exact tendsto_bot
no goals
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
this : ∀ (ε : ℝ), ε > 0 → ∃ I, ∀ (i : ι), i ≥ I → ‖↑(↑(orthogonalProjection (U i)) y) - y‖ < ε
⊢ Tendsto (fun i => ↑(↑(orthogonalProjection (U i)) x)) atTop
    (𝓝 ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x))
simpa only [proj_x, NormedAddCommGroup.tendsto_atTop] using this
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
y_mem : y ∈ Submodule.topologicalClosure (⨆ (i : ι), U i)
⊢ ∃ a, (a ∈ ⨆ (i : ι), U i) ∧ dist y a < ε
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
⊢ ∃ a, (a ∈ ⨆ (i : ι), U i) ∧ dist y a < ε
have y_mem : y ∈ (⨆ i, U i).topologicalClosure := Submodule.coe_mem _
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
y_mem : ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ ↑(⨆ (i : ι), U i) ∧ dist y b < ε
⊢ ∃ a, (a ∈ ⨆ (i : ι), U i) ∧ dist y a < ε
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
y_mem : y ∈ Submodule.topologicalClosure (⨆ (i : ι), U i)
⊢ ∃ a, (a ∈ ⨆ (i : ι), U i) ∧ dist y a < ε
rw [← SetLike.mem_coe, Submodule.topologicalClosure_coe, Metric.mem_closure_iff] at y_mem
no goals
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
y_mem : ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ ↑(⨆ (i : ι), U i) ∧ dist y b < ε
⊢ ∃ a, (a ∈ ⨆ (i : ι), U i) ∧ dist y a < ε
exact y_mem ε hε
no goals
𝕜 : Type u_3
E : Type u_1
F : Type ?u.850669
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✝ : ∀ (i : ι), CompleteSpace { x // x ∈ U i }
hU : Monotone U
x : E
h✝ : Nonempty ι
y : E := ↑(↑(orthogonalProjection (Submodule.topologicalClosure (⨆ (i : ι), U i))) x)
proj_x : ∀ (i : ι), ↑(orthogonalProjection (U i)) x = ↑(orthogonalProjection (U i)) y
ε : ℝ
hε : ε > 0
a : E
ha : a ∈ ⨆ (i : ι), U i
hay : ‖y - a‖ < ε
⊢ ∃ I, a ∈ U I
rwa [Submodule.mem_iSup_of_directed _ hU.directed_le] at ha