English
The Pi-orthonormalBasis B, when converted to a basis, equals the mapped basis obtained from the component bases via the global linear equivalence.
Русский
Переобразование Pi-ортонормBasis в базис совпадает с отображением базиса через компонентные базисы и глобальное линейное эквивалентное отображение.
LaTeX
$$$\Pi.\orthonormalBasis \! B).toBasis = ((\Pi.basis \! (i) ((B i).toBasis)).map( (WithLp.linearEquiv 2 𝕜 ( (j : η) → E j) ).symm)$$$
Lean4
theorem _root_.Pi.orthonormalBasis.toBasis {η : Type*} [Fintype η] {ι : η → Type*} [∀ i, Fintype (ι i)] {𝕜 : Type*}
[RCLike 𝕜] {E : η → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace 𝕜 (E i)]
(B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i)) :
(Pi.orthonormalBasis B).toBasis = ((Pi.basis fun i : η ↦ (B i).toBasis).map (WithLp.linearEquiv 2 _ _).symm) := by
ext; rfl
