span_gramSchmidt_Iic — Mathlib

English

Let f: ι → E. For every c, the span of the Gram–Schmidt vectors corresponding to indices i with i ≤ c coincides with the span of the original vectors with i ≤ c.

Русский

Пусть f: ι → E. Для любого c выполняется равенство спанов: порождающее множество из Gram–Schmidt на индексации i ≤ c образует тот же подпространство, что и исходные элементы f i с i ≤ c.

LaTeX

$$$$\operatorname{span}_{\mathbb{K}}\big(\mathrm{gramSchmidt}_{\mathbb{K}} f \,'\, \mathrm{Iic}(c)\big) = \operatorname{span}_{\mathbb{K}}\big( f \,'\, \mathrm{Iic}(c) \big).$$$$

Lean4

theorem span_gramSchmidt_Iic (f : ι → E) (c : ι) : span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic c) = span 𝕜 (f '' Set.Iic c) :=
  span_eq_span (Set.image_subset_iff.2 fun _ => gramSchmidt_mem_span _ _) <|
    Set.image_subset_iff.2 fun _ => mem_span_gramSchmidt _ _

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