English
Let E be a finite-dimensional inner product space over a field 𝕜 equipped with a decomposition V = (V_i)_{i∈ι} into an internal direct sum. Then there exists an orthonormal basis B = (b_1, …, b_n) of E, indexed by Fin(n), which is subordinate to this direct-sum decomposition; equivalently, there is a function φ: Fin(n) → ι such that b_j ∈ V_{φ(j)} for all j.
Русский
Пусть E — конечномерное пространство с внутренним скалярным произведением над полем 𝕜, разложенное как внутренное объединение E = ⊕_{i∈ι} V_i. Тогда существует ортонормированная база B = (b_1, ..., b_n) пространства E, индексируемая Fin(n), подчинённая этому разложению; то есть существует отображение φ: Fin(n) → ι такое, что b_j ∈ V_{φ(j)} для всех j.
LaTeX
$$$\\exists B = (b_j)_{j \\in \\mathrm{Fin}(n)} ,\\; B \\\\text{orthonormal in } E \\\\text{and } (\\exists \\phi: \\mathrm{Fin}(n) \\to ι) \\; (\\forall j,\\; b_j \\in V_{\\phi(j)})$$$
Lean4
/-- An `n`-dimensional `InnerProductSpace` equipped with a decomposition as an internal direct
sum has an orthonormal basis indexed by `Fin n` and subordinate to that direct sum. -/
def subordinateOrthonormalBasis :=
val_proj @wrapped✝.{}
