toIsometryEquiv_injective — Mathlib

English

Equality of toIsometryEquiv implies equality of the original LinearIsometryEquiv.

Русский

Равенство toIsometryEquiv влечет равенство исходной LinearIsometryEquiv.

LaTeX

$$$f^{\\mathrm{toIsometryEquiv}} = g^{\\mathrm{toIsometryEquiv}} \\Rightarrow f = g$$$

Lean4

theorem toIsometryEquiv_injective : Function.Injective (toIsometryEquiv : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ᵢ E₂) := fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toIsometryEquiv = _)

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