English
Composition of two order monoid isomorphisms is an order monoid isomorphism: trans preserves order and multiplication, and its underlying equivalence is the composition of the two.
Русский
Композицией двух упорядоченных моноидных изоморфизмов получается новый упорядоченный моноидный изоморфизм; сохраняются порядок и умножение.
LaTeX
$$$\\text{trans} : α \\simeq^*o γ \;\\text{from } α \\simeq^*o β, β \\simeq^*o γ$; it satisfies $\\text{toMulEquiv}(f.trans g) = (toMulEquiv f).trans (toMulEquiv g)$ and preserves map_le_map_iff'.$$
Lean4
/-- Transitivity of multiplication-preserving order isomorphisms -/
@[to_additive (attr := trans) /-- Transitivity of addition-preserving order isomorphisms -/
]
def trans (f : α ≃*o β) (g : β ≃*o γ) : α ≃*o γ :=
{ (f : α ≃* β).trans g with map_le_map_iff' := by simp }
