English
If s and t have the same length, Shortlex r s t holds exactly when Lex r s t holds.
Русский
Если длины списков s и t совпадают, Shortlex r s t выполняется тогда, когда выполняется Lex r s t.
LaTeX
$$$ \\forall {s t : List \\alpha}, \\mathrm{length}(s) = \\mathrm{length}(t) \\Rightarrow \\mathrm{Shortlex} \\ r \\ s \\ t \\iff \\mathrm{Lex} \\ r \\ s \\ t.$$$
Lean4
/-- If two lists `s` and `t` have the same length, `s` is smaller than `t` under the shortlex order
over a relation `r` when `s` is smaller than `t` under the lexicographic order over `r` -/
theorem of_lex {s t : List α} (len_eq : s.length = t.length) (h_lex : List.Lex r s t) : Shortlex r s t :=
by
apply Prod.lex_def.mpr
right
exact ⟨len_eq, h_lex⟩
