span_gramSchmidt_Iio — Mathlib

English

Let f: ι → E. For every c, the Gram–Schmidt vectors with indices i < c span the same space as the original vectors with i < c.

Русский

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

LaTeX

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

Lean4

theorem span_gramSchmidt_Iio (f : ι → E) (c : ι) : span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio c) = span 𝕜 (f '' Set.Iio c) :=
  span_eq_span
      (Set.image_subset_iff.2 fun _ hi =>
        span_mono (image_mono <| Iic_subset_Iio.2 hi) <| gramSchmidt_mem_span _ _ le_rfl) <|
    Set.image_subset_iff.2 fun _ hi => span_mono (image_mono <| Iic_subset_Iio.2 hi) <| mem_span_gramSchmidt _ _ le_rfl

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