toIsometryEquiv_inj — Mathlib

English

As a consequence of injectivity, the simplified form holds for isometry equivalence.

Русский

Следствием инъективности является упрощенная формулировка для эквивалентности по изометриям.

LaTeX

$$$\\text{simp}: f^{\\mathrm{toIsometryEquiv}} = g^{\\mathrm{toIsometryEquiv}} \\Rightarrow f = g$$$

Lean4

@[simp]
theorem toIsometryEquiv_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toIsometryEquiv = g.toIsometryEquiv ↔ f = g :=
  toIsometryEquiv_injective.eq_iff

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