toEquiv_inj — Mathlib

English

For any two coalgebra equivalences e1,e2: A ≃ₗc[R] B, equality of their underlying linear equivalences e1.toEquiv and e2.toEquiv holds iff e1 = e2.

Русский

Для любых двух коалгебраических эквивалентностей e1,e2: A ≃ₗc[R] B равенство их соответствующих линейных эквивленций e1.toEquiv и e2.toEquiv эквивалентно e1 = e2.

LaTeX

$$$e_1.toEquiv = e_2.toEquiv \\iff e_1 = e_2$$$

Lean4

@[simp]
theorem toEquiv_inj {e₁ e₂ : A ≃ₗc[R] B} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂ :=
  toEquiv_injective.eq_iff

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