mk_coe — Mathlib

English

Constructing an ordered monoid homomorphism from a function with a monotone witness yields the same object as the original with the given function.

Русский

Построение отображения из функции с доказательством монотонности даёт тот же объект, что и исходное отображение.

LaTeX

$$$OrderMonoidHom.mk f h = f$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_coe (f : α →*o β) (h) : OrderMonoidHom.mk (f : α →* β) h = f :=
  by
  ext
  rfl

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