trans — Mathlib

English

BialgEquiv are transitive: from A to B and B to C gives A to C.

Русский

Биалгебровые эквивалентности транзитивны: имеется переход из A в C через B.

LaTeX

$$$e_{13} = e_{12} \\;\\text{trans}\\; e_{23}$$$

Lean4

/-- Bialgebra equivalences are transitive. -/
@[trans, simps!]
def trans (e₁₂ : A ≃ₐc[R] B) (e₂₃ : B ≃ₐc[R] C) : A ≃ₐc[R] C :=
  { (e₁₂ : A ≃ₗc[R] B).trans (e₂₃ : B ≃ₗc[R] C), (e₁₂ : A ≃* B).trans (e₂₃ : B ≃* C) with }

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