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