ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.887976
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))) ≤
    topologicalClosure
      (span 𝕜 (⋃ (i : Finset ι), ↑(Finset.image (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)))
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.887976
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))) ≤
    topologicalClosure
      (⨆ (J : Finset ι), span 𝕜 ↑(Finset.image (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) J))
simp_rw [← Submodule.span_iUnion]
no goals
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.887976
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
⊢ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))) ≤
    topologicalClosure
      (span 𝕜 (⋃ (i : Finset ι), ↑(Finset.image (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i)))
exact topologicalClosure_mono (span_mono <| Set.range_subset_iff.mpr fun i =>
  Set.mem_iUnion_of_mem {i} <| Finset.mem_coe.mpr <| Finset.mem_image_of_mem _ <|
  Finset.mem_singleton_self i)