English
The orthonormal basis on a product space corresponds to a standard basis under a suitable isomorphism, i.e., the toBasis map aligns with the standard Basis under a linear isometry.
Русский
Ортонормированный базис на произведении пространств сходится к стандартному базису через изоморфизм, то есть сопоставление toBasis совпадает с обычным базисом через изометрическое отображение.
LaTeX
$$$(Pi.orthonormalBasis B).toBasis = ((Pi.basis (\\lambda i. (B i).toBasis)).map (WithLp.linearEquiv 2 _ _).symm)$$$
Lean4
/-- Mapping an orthonormal basis along a `LinearIsometryEquiv`. -/
protected def map {G : Type*} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E)
(L : E ≃ₗᵢ[𝕜] G) : OrthonormalBasis ι 𝕜 G where repr := L.symm.trans b.repr
