to_ne — Mathlib

English

If a Lexicographic comparison between two lists is established via Ne (not equal), then the lists are indeed distinct.

Русский

Если лексикографическое сравнение двух списков устанавливается через неравенство, значит списки различны.

LaTeX

$$$\forall {l_1 l_2 : List\;\alpha},\; List.Lex (fun x y => Ne x y) l_1 l_2 \rightarrow l_1 \neq l_2$$$

Lean4

theorem to_ne : ∀ {l₁ l₂ : List α}, Lex (· ≠ ·) l₁ l₂ → l₁ ≠ l₂
  | _, _, cons h, e => to_ne h (List.cons.inj e).2
  | _, _, rel r, e => r (List.cons.inj e).1

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