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