coe_mk — Mathlib

English

Let f be an ordered monoid with zero homomorphism α →*₀o β, together with a witnessing monotone map h. Then the underlying function of the construction OrderMonoidWithZeroHom.mk f h is exactly f.

Русский

Пусть f — упорядоченный гомоморфизм моноида с нулём, α →*₀o β, и дано монотонное доказательство h. Тогда базовая функция конструкции OrderMonoidWithZeroHom.mk f h равна f.

LaTeX

$$$\big(\mathrm{OrderMonoidWithZeroHom.mk}(f,h) : \alpha \to \beta\big) = f$$$

Lean4

@[simp]
theorem coe_mk (f : α →*₀ β) (h) : (OrderMonoidWithZeroHom.mk f h : α → β) = f :=
  rfl

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