English
The first-coordinate projection from Lex(α × β) to α is the natural projection onto the α-component in the lexicographic product.
Русский
Первая координатная проекция из Lex(α × β) в α представляет собой естественную проекцию на компоненту α в лексикографическом произведении.
LaTeX
$$$$ fst_{Lex}: Lex(\alpha,\beta) \to \alpha,\quad fst_{Lex}( (a,b) ) = a. $$$$
Lean4
/-- Given ordered monoids M, N, the natural projection ordered homomorphism from the
lexicographic M ×ₗ N to M. -/
@[to_additive (attr := simps!) /-- Given ordered additive monoids M, N, the natural projection
ordered homomorphism from the lexicographic M ×ₗ N to M. -/
]
def fstₗ : (α ×ₗ β) →*o α where
toFun p := (ofLex p).fst
map_one' := rfl
map_mul' := by simp
monotone' := Prod.Lex.monotone_fst_ofLex
