toMonoidWithZeroHom_coe — Mathlib

English

Let f: β →*₀o γ and g: α →*₀o β be order-monoid-with-zero-homomorphisms. Then the composition f ∘ g, viewed as an order-monoid-with-zero-homomorphism α →*₀o γ, is equal to composing f (as β →*₀o γ) with g; i.e., (f.comp g) = (f : β →*₀o γ).comp g.

Русский

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

LaTeX

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

Lean4

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

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