English
If α has a unique element and N is ordered, then for any a,b in Lex(α →₀ N), a < b holds if and only if the value at the unique element in a is less than the corresponding value in b.
Русский
Если у α имеется единственный элемент, и N упорядочено, то для любых a,b ∈ Lex(α →₀ N) выполняется a < b тогда и только тогда, когда значение на единственном элементе в a меньше значения на этом элементе в b.
LaTeX
$$$a < b \\iff \\operatorname{ofLex} a \\mathrm{default} < \\operatorname{ofLex} b \\mathrm{default}$$$
Lean4
theorem lex_lt_iff_of_unique [Preorder α] [LT N] [Unique α] {a b : Lex (α →₀ N)} :
a < b ↔ ofLex a default < ofLex b default :=
by
simp only [lex_lt_iff, Unique.exists_iff, and_iff_right_iff_imp]
refine fun _ j hj ↦ False.elim (lt_irrefl j ?_)
simpa only [Unique.uniq] using hj
