English
Any finite subset of an orthonormal family forms an orthonormal basis for its span.
Русский
Любое конечное подмножество ортонормированной семейства образует ортонормированную базу для своего линейного замкнутого пространства.
LaTeX
$$$$ \\text{Let } h \\text{ be orthonormal and } s \\text{ a finite subset; then } \\mathrm{span}(s) \\text{ has an orthonormal basis } \\mathrm{span}(h,s). $$$$
Lean4
/-- Any finite subset of an orthonormal family is an `OrthonormalBasis` for its span. -/
protected def span [DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι') :
OrthonormalBasis s 𝕜 (span 𝕜 (s.image v' : Set E)) :=
let e₀' : Basis s 𝕜 _ := Basis.span (h.linearIndependent.comp ((↑) : s → ι') Subtype.val_injective)
let e₀ : OrthonormalBasis s 𝕜 _ :=
OrthonormalBasis.mk
(by
convert orthonormal_span (h.comp ((↑) : s → ι') Subtype.val_injective)
simp [e₀', Basis.span_apply])
e₀'.span_eq.ge
let φ : span 𝕜 (s.image v' : Set E) ≃ₗᵢ[𝕜] span 𝕜 (range (v' ∘ ((↑) : s → ι'))) :=
LinearIsometryEquiv.ofEq _ _
(by
rw [Finset.coe_image, image_eq_range]
rfl)
e₀.map φ.symm
