English
In Lex(α × β), the projection onto the second coordinate is an order-preserving monoid homomorphism from Lex(α × β) to β.
Русский
В Lex(α × β) проекция на вторую координату сохраняет порядок и является моноид-гомоморфизмом от Lex(α × β) к β.
LaTeX
$$$$ snd_{Lex}: Lex(\alpha,\beta) \to \beta \text{ with } snd_{Lex}( (a,b) ) = b. $$$$
Lean4
/-- Given ordered monoids M, N, the natural projection ordered homomorphism from M × N to N. -/
@[to_additive (attr := simps!) /-- Given ordered additive monoids M, N, the natural projection
ordered homomorphism from M × N to N. -/
]
def snd : α × β →*o β where
__ := MonoidHom.snd _ _
monotone' := MonoidHom.snd_mono
