coe_comp_orderHom — Mathlib

English

The composition viewed as an OrderHom equals the composition of the underlying OrderHom maps.

Русский

Композиция, рассматриваемая как отображение порядка, равна композиции соответствующих отображений порядка.

LaTeX

$$$ (f\comp g) = (f:\mathrm{OrderHom}(\beta,\gamma)).\circ (g:\mathrm{OrderHom}(\alpha,\beta)) $$$

Lean4

@[simp]
theorem coe_comp_orderHom (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) :
    (f.comp g : OrderHom α γ) = (f : OrderHom β γ).comp g :=
  rfl

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