finite_spans_dense — Mathlib

English

The series ∑_i ⟪x, b_i⟫ ⟪b_i, y⟫ converges to ⟪x, y⟫.

Русский

Ряд ∑_i ⟪x, b_i⟫ ⟪b_i, y⟫ сходится к ⟪x, y⟫.

LaTeX

$$$ HasSum (\\lambda i, ⟪x, b_i⟫ · ⟪b_i, y⟫) ⟪x, y⟫ $$$

Lean4

theorem finite_spans_dense [DecidableEq E] (b : HilbertBasis ι 𝕜 E) :
    (⨆ J : Finset ι, span 𝕜 (J.image b : Set E)).topologicalClosure = ⊤ :=
  eq_top_iff.mpr <|
    b.dense_span.ge.trans
      (by
        simp_rw [← Submodule.span_iUnion]
        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))

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