English
Let E be a product of inner product spaces E_i with i in η, and for each i an orthonormal basis B_i of E_i. Then the representation map of the product basis (Pi-orthonormalBasis B) applied to a vector x ∈ ∏ E_i, at index j = (i, α), equals the representation of B_i on x_i at index α. In other words, coordinates are taken componentwise.
Русский
Пусть E = ∏_{i∈η} E_i — произведение евклидовых пространств с соответствующими ортонормированными базами B_i. Тогда представление базиса произведения (Pi-orthonormalBasis B) для вектора x = (x_i) ⱼ (с индексами j = (i, α)) по координате j равно представлению базиса B_i для x_i по координате α. То есть координаты строятся по каждой компоненте отдельно.
LaTeX
$$$$ (\\mathrm{Pi\\text{-}orthonormalBasis} \\; B).\\mathrm{repr}(x)(i,\\alpha) = (B_i).\\mathrm{repr}(x_i)(\\alpha) $$$$
Lean4
@[simp]
theorem _root_.Pi.orthonormalBasis_repr {η : Type*} [Fintype η] {ι : η → Type*} [∀ i, Fintype (ι i)] {𝕜 : Type*}
[RCLike 𝕜] {E : η → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace 𝕜 (E i)]
(B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i)) (x : (i : η) → E i) (j : (i : η) × (ι i)) :
(Pi.orthonormalBasis B).repr x j = (B j.fst).repr (x j.fst) j.snd :=
rfl
