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