Theorems · Theorem · functional analysis

Orthonormal.exists_orthonormalBasis_extension

∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v : Set E} [FiniteDimensional 𝕜 E], Orthonormal 𝕜 Subtype.val → ∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val

In a finite-dimensional InnerProductSpace, any orthonormal subset can be extended to an orthonormal basis.

Defined in

Mathlib.Analysis.InnerProductSpace.PiL2

Cited by

2 results in Mathlib

Foundations

Depth 233 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensional