map_apply — Mathlib

English

Mapping an orthonormal basis along a linear isometry: given an ONB b of E and a linear isometry L: E ≃ᵢ G, the mapped basis b.map L is an orthonormal basis of G with repr transported by L.

Русский

Перенос ортонормированного базиса через линейное изометрическое отображение: b.map L образует ортонормированный базис в G с переносом представления через L.

LaTeX

$$$\text{b.map } L \text{ is ONB in } G$ with repr = L^{-1} ∘ b.repr$$

Lean4

@[simp]
protected theorem map_apply {G : Type*} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E)
    (L : E ≃ₗᵢ[𝕜] G) (i : ι) : b.map L i = L (b i) :=
  rfl

Похожие утверждения