ne_iff — Mathlib

English

For lists l1,l2 with length relation le(l1.length, l2.length), Lex (≠) l1 l2 iff l1 ≠ l2.

Русский

Для списков l1,l2 при условии длины l1 ≤ l2, Lex (≠) l1 l2 эквивалентно l1 ≠ l2.

LaTeX

$$$\\forall l_1\\ l_2\\ (\\mathrm{length}\\ l_1 \\le \\mathrm{length}\\ l_2)\\Rightarrow\\ \\mathrm{Lex}(\\neq)\\ l_1\\ l_2 \\iff l_1 \\neq l_2.$$$

Lean4

theorem ne_iff {l₁ l₂ : List α} (H : length l₁ ≤ length l₂) : Lex (· ≠ ·) l₁ l₂ ↔ l₁ ≠ l₂ := by
  classical exact Decidable.List.Lex.ne_iff H

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