English
Given ordered monoids M and N, the natural inclusion map a ↦ (a, 1) from M to M × N is an order-preserving monoid homomorphism (i.e., an order embedding).
Русский
Пусть заданы упорядоченные моноиды M и N. Натуральное включение a ↦ (a, 1) из M в M × N является моноид-гомоморфизм, сохраняющим порядок (то есть вложение по порядку).
LaTeX
$$$$ a \le a' \Rightarrow (a,1) \le (a',1). $$$$
Lean4
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to M × N. -/
@[to_additive (attr := simps!) /-- Given ordered additive monoids M, N, the natural inclusion
ordered homomorphism from M to M × N. -/
]
def inl : α →*o α × β where
__ := MonoidHom.inl _ _
monotone' := MonoidHom.inl_mono
