mem_span_gramSchmidt — Mathlib

English

In a normed space, PosDef (gram 𝕜 v) if and only if LinearIndependent 𝕜 v.

Русский

В нормированном пространстве PosDef(gram 𝕜 v) эквивалентно LinearIndependent(𝕜 v).

LaTeX

$$$ \text{PosDef }( \text{gram } 𝕜 v) \iff \text{LinearIndependent } 𝕜 v $$$

Lean4

theorem mem_span_gramSchmidt (f : ι → E) {i j : ι} (hij : i ≤ j) : f i ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j) :=
  by
  rw [gramSchmidt_def' 𝕜 f i]
  simp_rw [starProjection_singleton]
  exact
    Submodule.add_mem _ (subset_span <| mem_image_of_mem _ hij)
      (Submodule.sum_mem _ fun k hk =>
        smul_mem (span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)) _ <|
          subset_span <| mem_image_of_mem (gramSchmidt 𝕜 f) <| (Finset.mem_Iio.1 hk).le.trans hij)

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