not_shortlex_nil_right — Mathlib

English

For any list s, Shortlex r s [] is false; i.e., no list is strictly smaller than the empty list under Shortlex.

Русский

Для любого списка s Shortlex r s [] ложно; то есть ни один список не меньше пустого списка по Shortlex.

LaTeX

$$$ \\forall s : List \\alpha, \\neg \\mathrm{Shortlex} \\ r \\ s \\ [].$$$

Lean4

@[simp]
theorem not_shortlex_nil_right {s : List α} : ¬Shortlex r s [] :=
  by
  rw [shortlex_def]
  rintro (h1 | h2)
  · simp only [List.length_nil, not_lt_zero'] at h1
  · exact List.not_lex_nil h2.2

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