shortlex_cons_iff — Mathlib

English

If the relation r is irreflexive, then Shortlex r (a :: s) (a :: t) holds iff Shortlex r s t.

Русский

Если отношение r иррефлексивно, то Shortlex r (a :: s) (a :: t) выполняется тогда и только тогда, когда Shortlex r s t.

LaTeX

$$$ \\forall {α} {r}, [IsIrrefl \\ α \\ r] \\Rightarrow \\mathrm{Shortlex} \\ r (a :: s) (a :: t) \\iff \\mathrm{Shortlex} \\ r s t.$$$

Lean4

theorem shortlex_cons_iff [IsIrrefl α r] {a : α} {s t : List α} : Shortlex r (a :: s) (a :: t) ↔ Shortlex r s t := by
  simp only [shortlex_def, length_cons, add_lt_add_iff_right, add_left_inj, List.lex_cons_iff]

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