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