coe_toLinearEquiv — Mathlib

English

The function that gives the linear isometry from the isometry equivalence is injective.

Русский

Функция, сопоставляющая изометрическую эквивалентность линейной изометрии, инъективна.

LaTeX

$$$\\mathrm{coe}_{\\mathrm{LI}}(e) = \\mathrm{coe}_{\\mathrm{LI}}(f) \\Rightarrow e = f$$$

Lean4

@[simp]
theorem coe_toLinearEquiv (e : E ≃ₛₗᵢ[σ₁₂] E₂) : ⇑e.toLinearEquiv = e :=
  rfl

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