English
The natural inclusion of α into the lexicographic lex-ordered product Lex(α × β) is an order-preserving monoid homomorphism, given by m ↦ (m, 1) in the lexicographic order.
Русский
Естественное вложение α в лексикографическое произведение Lex(α × β) сохраняет порядок и является моноид-гомоморфизмом, отображая m ↦ (m,1).
LaTeX
$$$$ inl_{Lex}(m) = (m,1),\quad f\_1(m) \le f\_1(m') \text{ if } m \le m'. $$$$
Lean4
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to the
lexicographic M ×ₗ N. -/
@[to_additive (attr := simps!) /-- Given ordered additive monoids M, N, the natural inclusion
ordered homomorphism from M to the lexicographic M ×ₗ N. -/
]
def inlₗ : α →*o α ×ₗ β where
__ := (Prod.Lex.toLexOrderHom).comp (inl α β)
map_one' := rfl
map_mul' := by simp [← toLex_mul]
