toLinearEquiv_injective — Mathlib

English

The map that sends a LinearIsometryEquiv to its underlying LinearEquiv is injective: if two such objects have the same underlying LinearEquiv, they are equal.

Русский

Отображение, переводящее линейную изометрическую эквивалентность к базовому линейному эквиваленту, инъективно: если две такие сущности имеют один и тот же базовый линейный эквивалент, они равны.

LaTeX

$$$\\text{toLinearEquiv}: (E \\simeq_{\\mathrm{LI}} E') \\to (E \\simeq E') \\quad \\text{соотношение инъективно}$$$

Lean4

theorem toLinearEquiv_injective : Injective (toLinearEquiv : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ₛₗ[σ₁₂] E₂)
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

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