repr_injective — Mathlib

English

The map sending an orthonormal basis to its representation in EuclideanSpace is injective; i.e., distinct orthonormal bases have distinct representations.

Русский

Отображение ортонормированного базиса в его представление в EuclideanSpace инъективно: разные базисы дают разные представления.

LaTeX

$$Injective (repr : OrthonormalBasis ι 𝕜 E → EuclideanSpace 𝕜 ι)$$

Lean4

theorem repr_injective : Injective (repr : OrthonormalBasis ι 𝕜 E → E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) := fun f g h =>
  by
  cases f
  cases g
  congr

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