English
The span of the Hilbert basis vectors is dense in the ambient space E.
Русский
Гильбертовая база порождает плотное подпространство в E.
LaTeX
$$$ \\overline{\\mathrm{span}_{𝕂}(\\{b_i : i \\in ι\\})} = E $$$
Lean4
@[simp]
protected theorem dense_span (b : HilbertBasis ι 𝕜 E) : (span 𝕜 (Set.range b)).topologicalClosure = ⊤ := by
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⟩