span_gramSchmidt — Mathlib

English

The span of the Gram–Schmidt family equals the span of the original family: Gram–Schmidt does not change the span of the set.

Русский

Пусть f: ι → E. Множество векторов, получаемых через Gram–Schmidt, порождает то же подпространство, что и исходное множество {f i}.

LaTeX

$$$$\operatorname{span}_{\mathbb{K}}\big(\mathrm{range}(\mathrm{gramSchmidt}_{\mathbb{K}} f)\big) = \operatorname{span}_{\mathbb{K}}\big(\mathrm{range}(f)\big).$$$$

Lean4

/-- `gramSchmidt` preserves span of vectors. -/
theorem span_gramSchmidt (f : ι → E) : span 𝕜 (range (gramSchmidt 𝕜 f)) = span 𝕜 (range f) :=
  span_eq_span (range_subset_iff.2 fun _ => span_mono (image_subset_range _ _) <| gramSchmidt_mem_span _ _ le_rfl) <|
    range_subset_iff.2 fun _ => span_mono (image_subset_range _ _) <| mem_span_gramSchmidt _ _ le_rfl

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