coe_comp_orderHom — Mathlib

English

The order-homomorphism underlying the composite equals the composition of the underlying order-homomorphisms.

Русский

Подлежащий порядковый гомоморфизм составного отображения равен композиции порядковых гомоморфизмов.

LaTeX

$$$\mathrm{toOrderHom}(g\circ f) = \mathrm{toOrderHom}(g) \circ \mathrm{toOrderHom}(f)$$$

Lean4

@[simp]
theorem coe_comp_orderHom (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :
    (g.comp f : α →o γ) = (g : β →o γ).comp f :=
  rfl

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