toOrderMonoidHom_injective — Mathlib

English

There exists a natural map from ordered monoid with zero homomorphisms to order monoid homomorphisms that preserves structure and whose underlying function equals the original f.

Русский

Существует естественная карта от упорядоченных гомоморфизмов моноида с нулём к обычным моноидогомоморфизмам, сохраняющая структуру и совпадающая по функции с исходной f.

LaTeX

$$$\operatorname{toOrderMonoidHom}(f) = f \quad\text{(as functions)}$$$

Lean4

theorem toOrderMonoidHom_injective : Injective (toOrderMonoidHom : _ → α →*o β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

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