English
If two lists have equal length, Shortlex r s t is equivalent to Lex r s t.
Русский
Если два списка имеют одинаковую длину, Shortlex r s t эквивалентен Lex r s t.
LaTeX
$$$ \\forall {s t : List \\alpha}, |s| = |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` exactly when `s` is smaller than `t` under the lexicographic order over `r`. -/
theorem shortlex_iff_lex {s t : List α} (h : s.length = t.length) : Shortlex r s t ↔ List.Lex r s t := by
simp [shortlex_def, h]