English
Let ι be linearly ordered and α_i linearly ordered with zero; consider the lexicographic order on the finitely supported functions; the relation < on this lex order is decidable.
Русский
Пусть ι линейно упорядочено, для каждого i α_i линейно упорядовано с нулём; рассмотрим лексикографический порядок на множество функций с конечной опорой; отношение < в этом порядке разрешимо.
LaTeX
$$$\\\\mathrm{DecidableLT}(\\\\mathrm{Lex}(\\\\Pi_{i\\in I} \\alpha_i))$$$
Lean4
/-- The less-than relation for the lexicographic ordering is decidable. -/
instance decidableLT : DecidableLT (Lex (Π₀ i, α i)) :=
lt_trichotomy_rec (fun h ↦ isTrue h) (fun h ↦ isFalse h.not_lt) fun h ↦ isFalse h.asymm
