shortlex_iff_lex — Mathlib

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]

Похожие утверждения