English
The composition of two bounded-order homomorphisms is again a bounded-order homomorphism.
Русский
Состав двух отображений, сохраняющих порядок и границы, является отображением, сохраняющим порядок и границы.
LaTeX
$$$f:\mathrm{BoundedOrderHom}(\beta,\gamma),\; g:\mathrm{BoundedOrderHom}(\alpha,\beta)\quad \Rightarrow\quad f \circ g \in \mathrm{BoundedOrderHom}(\alpha,\gamma)$$$
Lean4
/-- Composition of `BoundedOrderHom`s as a `BoundedOrderHom`. -/
def comp (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : BoundedOrderHom α γ :=
{ f.toOrderHom.comp g.toOrderHom, f.toTopHom.comp g.toTopHom, f.toBotHom.comp g.toBotHom with }
