toEquiv_inj — Mathlib

English

The map from a bialgebra equivalence to its underlying type equivalence is injective.

Русский

Отображение биалгебровой эквивалентности к соответствующей эквивалентности типов инъективно.

LaTeX

$$$\\text{toEquiv}: (A \\simeq_{bialg} B) \\to (A \\simeq B)$ injective$$

Lean4

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

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