toOrderMonoidHom_comp — Mathlib

English

Let f: β →*₀o γ and g: α →*₀o β. Then the composition f ∘ g, viewed as an OrderMonoidWithZeroHom α →*₀o γ, equals the composition of f (viewed as β →*₀o γ) with g; i.e., (f.comp g) = (f : β →*₀o γ).comp g.

Русский

Пусть f: β →*₀o γ и g: α →*₀o β. Тогда композиция f ∘ g, как OrderMonoidWithZeroHom α →*₀o γ, равна композиции f (как β →*₀o γ) и g.

LaTeX

$$$ (f.comp g : α →*₀o γ) = (f : β →*₀o γ).comp g $$$

Lean4

@[simp]
theorem toOrderMonoidHom_comp (f : β →*₀o γ) (g : α →*₀o β) : (f.comp g : α →*o γ) = (f : β →*o γ).comp g :=
  rfl

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