coe_comp_orderHom — Mathlib

English

Let f: β →*o γ and g: α →*o β be order-preserving monoid homomorphisms. The composition regarded as an order-preserving map equals the composition of the underlying order-homomorphisms: (f.comp g) = (f : β →o γ).comp g.

Русский

Пусть f: β →*o γ и g: α →*o β — упорядоченные моноид-гомоморфизмы. Композиция рассматривается как отображение, сохраняющее порядок, и эквивалентна композиции их соответствующих отображений порядка.

LaTeX

$$$ (f.comp g : α \too γ) = (f : β \too γ).comp g $$$

Lean4

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

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