toMonoidWithZeroHom_mk — Mathlib

English

Let f be a monotone monoid-with-zero-homomorphism f: α →*₀ β with hf : Monotone f. Then the order-preserving extension built from f, denoted OrderMonoidWithZeroHom.mk f hf, has the same underlying map as f; i.e., it equals f.

Русский

Пусть f : α →*₀ β является монотонным гомоморфизмом моноида с нулём, hf : Monotone f. Тогда конструкция OrderMonoidWithZeroHom.mk f hf имеет ту же исходную функцию, что и f; то есть равна f.

LaTeX

$$$((\\mathrm{OrderMonoidWithZeroHom.mk}\,f\,hf) : \\alpha \\to*₀ \\beta) = f$$$

Lean4

@[simp]
theorem toMonoidWithZeroHom_mk (f : α →*₀ β) (hf : Monotone f) : ((OrderMonoidWithZeroHom.mk f hf) : α →*₀ β) = f := by
  rfl

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