English
For the constructed subordinate orthonormal basis, each basis vector lies in the corresponding subspace of the internal direct sum.
Русский
Для построенной подчинённой ортонормированной базы каждый базисный вектор лежит в соответствующем подпространстве внутреннего прямого разложения.
LaTeX
$$$\forall a: Fin(n),\; hV.subordinateOrthonormalBasis hn hV' a \in V (hV.subordinateOrthonormalBasisIndex hn hV' a)$$$
Lean4
/-- The basis constructed in `DirectSum.IsInternal.subordinateOrthonormalBasis` is subordinate to
the `OrthogonalFamily` in question. -/
theorem subordinateOrthonormalBasis_subordinate (a : Fin n)
(hV' : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) :
hV.subordinateOrthonormalBasis hn hV' a ∈ V (hV.subordinateOrthonormalBasisIndex hn a hV') := by
simpa only [DirectSum.IsInternal.subordinateOrthonormalBasis, OrthonormalBasis.coe_reindex,
DirectSum.IsInternal.subordinateOrthonormalBasisIndex] using
hV.collectedOrthonormalBasis_mem hV' (fun i => stdOrthonormalBasis 𝕜 (V i))
((hV.sigmaOrthonormalBasisIndexEquiv hn hV').symm a)
