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.844341
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))) = ⊤
classical
  rw [eq_top_iff]
  rintro x -
  refine' mem_closure_of_tendsto (b.hasSum_repr x) (eventually_of_forall _)
  intro s
  simp only [SetLike.mem_coe]
  refine' sum_mem _
  rintro i -
  refine' smul_mem _ _ _
  exact subset_span ⟨i, rfl⟩
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
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)))
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
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))) = ⊤
rw [eq_top_iff]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ x ∈ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
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)))
rintro x -
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ ∀ (x_1 : Finset ι),
    ∑ b_1 in x_1, (fun i => ↑(↑b.repr x) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) b_1 ∈
      ↑(span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ x ∈ topologicalClosure (span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
refine' mem_closure_of_tendsto (b.hasSum_repr x) (eventually_of_forall _)
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ b_1 in s, (fun i => ↑(↑b.repr x) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) b_1 ∈
    ↑(span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ ∀ (x_1 : Finset ι),
    ∑ b_1 in x_1, (fun i => ↑(↑b.repr x) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) b_1 ∈
      ↑(span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
intro s
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ x_1 in s, ↑(↑b.repr x) x_1 • ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 x_1 1) ∈
    span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ b_1 in s, (fun i => ↑(↑b.repr x) i • (fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)) i) b_1 ∈
    ↑(span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1)))
simp only [SetLike.mem_coe]
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∀ (c : ι),
    c ∈ s →
      ↑(↑b.repr x) c • ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 c 1) ∈
        span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ x_1 in s, ↑(↑b.repr x) x_1 • ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 x_1 1) ∈
    span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
refine' sum_mem _
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ ↑(↑b.repr x) i • ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1) ∈
    span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∀ (c : ι),
    c ∈ s →
      ↑(↑b.repr x) c • ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 c 1) ∈
        span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
rintro 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.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1) ∈
    span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type ?u.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ ↑(↑b.repr x) i • ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1) ∈
    span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
refine' smul_mem _ _ _
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.844341
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
i : ι
⊢ ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1) ∈
    span 𝕜 (Set.range fun i => ↑(LinearIsometryEquiv.symm b.repr) (lp.single 2 i 1))
exact subset_span ⟨i, rfl⟩