toEquiv_injective — Mathlib

English

The map sending a bialgebra equivalence to its underlying bialg hom is injective.

Русский

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

LaTeX

$$$\\text{toBialgHom}: (A \\simeq_{bialg} B) \\to (A \\to_{bialg} B)$ is injective$$

Lean4

theorem toEquiv_injective : Function.Injective (toEquiv : (A ≃ₐc[R] B) → A ≃ B) := fun ⟨_, _⟩ ⟨_, _⟩ h =>
  (BialgEquiv.mk.injEq _ _ _ _).mpr (CoalgEquiv.toEquiv_injective h)

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