exists_orthonormalBasis — Mathlib

English

Every finite-dimensional inner product space has an orthonormal basis.

Русский

Любое конечномерное пространство с скалярным произведением имеет ортонормированный базис.

LaTeX

$$$\exists w\;\exists b\, (w ⊆ E) \, (b\; :\; OrthonormalBasis w 𝕜 E), \; ⇑b = ((↑) : w → E)$$$

Lean4

/-- A finite-dimensional inner product space admits an orthonormal basis. -/
theorem _root_.exists_orthonormalBasis : ∃ (w : Finset E) (b : OrthonormalBasis w 𝕜 E), ⇑b = ((↑) : w → E) :=
  let ⟨w, hw, _, hw''⟩ := (orthonormal_empty 𝕜 E).exists_orthonormalBasis_extension
  ⟨w, hw, hw''⟩

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