English
The lexicographic order induces a preorder on α × β; the relation is reflexive and transitive.
Русский
Лексикографический порядок порождает на α × β отношение предупорядоченности: рефлексивность и транзитивность выполняются.
LaTeX
$$$$ \le_{\mathrm{lex}} \text{ на } \alpha \times \beta \text{ определяет множество отношений, удовлетворяющих свойствам предупорядоченности.} $$$$
Lean4
/-- Dictionary / lexicographic preorder for pairs. -/
instance instPreorder (α β : Type*) [Preorder α] [Preorder β] : Preorder (α ×ₗ β)
where
le_refl := refl_of <| Prod.Lex _ _
le_trans _ _ _ := trans_of <| Prod.Lex _ _
lt_iff_le_not_ge x₁ x₂ := by aesop (add simp [le_iff, lt_iff, lt_iff_le_not_ge])
