of_length_lt — Mathlib

English

If s and t have equal length, then s is smaller than t under Shortlex if and only if s is smaller than t under Lex.

Русский

Если длины списков s и t равны, то s < Shortlex t тогда и только тогда, когда s < Lex 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 a list `s` is shorter than a list `t`, then `s` is smaller than `t` under any shortlex
order. -/
theorem of_length_lt {s t : List α} (h : s.length < t.length) : Shortlex r s t :=
  Prod.Lex.left _ _ h

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