toBasis_map — Mathlib

English

The map between orthonormal bases preserves the basis structure: mapping an ONB via a linear isometry yields a basis that is compatible with the map on bases.

Русский

Перемещение базиса через изометрическое отображение сохраняет структуру базиса.

LaTeX

$$$(b.map L).toBasis = b.toBasis$ under appropriate identifications$$

Lean4

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

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