English
In a finite-dimensional inner product space, any orthonormal set can be extended to an orthonormal basis.
Русский
В конечноразмерном пространстве с скалярным произведением любая ортонормированная подмножество может быть дополнено до ортонормированного базиса.
LaTeX
$$Exists (u : Finset E) (b : OrthonormalBasis u 𝕜 E), v ⊆ u ∧ ⇑b = ((↑) : u → E)$$
Lean4
/-- In a finite-dimensional `InnerProductSpace`, any orthonormal subset can be extended to an
orthonormal basis. -/
theorem exists_orthonormalBasis_extension (hv : Orthonormal 𝕜 ((↑) : v → E)) :
∃ (u : Finset E) (b : OrthonormalBasis u 𝕜 E), v ⊆ u ∧ ⇑b = ((↑) : u → E) :=
by
obtain ⟨u₀, hu₀s, hu₀, hu₀_max⟩ := exists_maximal_orthonormal hv
rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hu₀] at hu₀_max
have hu₀_finite : u₀.Finite := hu₀.linearIndependent.setFinite
let u : Finset E := hu₀_finite.toFinset
let fu : ↥u ≃ ↥u₀ := hu₀_finite.subtypeEquivToFinset.symm
have hu : Orthonormal 𝕜 ((↑) : u → E) := by simpa using hu₀.comp _ fu.injective
refine ⟨u, OrthonormalBasis.mkOfOrthogonalEqBot hu ?_, ?_, ?_⟩
· simpa [u] using hu₀_max
· simpa [u] using hu₀s
· simp
