English
In the real setting, the inner product with basisFun i yields the i-th coordinate.
Русский
В вещественном случае скалярное произведение с basisFun i даёт i-ю координату.
LaTeX
$$$$ \\langle x, \\mathrm{basisFun}_{\\mathbb{R}}(i) \\rangle = x_i. $$$$
Lean4
/-- Given an internal direct sum decomposition of a module `M`, and an orthonormal basis for each
of the components of the direct sum, the disjoint union of these orthonormal bases is an
orthonormal basis for `M`. -/
noncomputable def collectedOrthonormalBasis (hV : OrthogonalFamily 𝕜 (fun i => A i) fun i => (A i).subtypeₗᵢ)
[DecidableEq ι] (hV_sum : DirectSum.IsInternal fun i => A i) {α : ι → Type*} [∀ i, Fintype (α i)]
(v_family : ∀ i, OrthonormalBasis (α i) 𝕜 (A i)) : OrthonormalBasis (Σ i, α i) 𝕜 E :=
(hV_sum.collectedBasis fun i => (v_family i).toBasis).toOrthonormalBasis <| by
simpa using hV.orthonormal_sigma_orthonormal (show ∀ i, Orthonormal 𝕜 (v_family i).toBasis by simp)
