𝕜 : Type u_2
E : Type u_1
F : Type ?u.2158643
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2158692
dec_ι : DecidableEq ι
s : Set (Set E)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set E), a ∈ s → Orthonormal 𝕜 fun x => ↑x
⊢ Orthonormal 𝕜 fun x => ↑x
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2158643
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2158692
dec_ι : DecidableEq ι
s : Set (Set E)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set E), a ∈ s → Orthonormal 𝕜 fun x => ↑x
⊢ Orthonormal 𝕜 fun x => ↑x
rw [Set.sUnion_eq_iUnion]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2158643
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2158692
dec_ι : DecidableEq ι
s : Set (Set E)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set E), a ∈ s → Orthonormal 𝕜 fun x => ↑x
⊢ Orthonormal 𝕜 fun x => ↑x
exact orthonormal_iUnion_of_directed hs.directed_val (by simpa using h)
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.2158643
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2158692
dec_ι : DecidableEq ι
s : Set (Set E)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set E), a ∈ s → Orthonormal 𝕜 fun x => ↑x
⊢ ∀ (i : ↑s), Orthonormal 𝕜 fun x => ↑x
simpa using h