English
Let ι be a linearly ordered index set and let α_i be linearly ordered sets with a distinguished zero element for every i. Consider the lexicographic order on the finitely supported functions f: ι → α_i. Then the relation ≤ on this lexicographic order is decidable.
Русский
Пусть ι — линейно упорядоченная индексная множество, для каждого i задано линейно упорядоченное множество α_i с выделенным нулём; рассмотрим лексикографический порядок на множество finitely supported функций f: ι → α_i. Тогда отношение ≤ в этом лексикографическом порядке разрешимо.
LaTeX
$$$\\\\mathrm{DecidableLE}(\\\\mathrm{Lex}(\\\\Pi_{i\\in I} \\alpha_i))$$$
Lean4
/-- The less-or-equal relation for the lexicographic ordering is decidable. -/
instance decidableLE : DecidableLE (Lex (Π₀ i, α i)) :=
lt_trichotomy_rec (fun h ↦ isTrue <| Or.inr h) (fun h ↦ isTrue <| Or.inl <| congr_arg _ h) fun h ↦
isFalse fun h' ↦ lt_irrefl _ (h.trans_le h')
