dense_span — Mathlib

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⟩

Похожие утверждения