lex_cons_iff — Mathlib

English

For any relation r with IsIrrefl, Lex r (a :: l1) (a :: l2) is equivalent to Lex r l1 l2. In particular, repeating the head does not affect the lexicographic comparison when the heads are equal.

Русский

При связи r, если r irréfléchis, то Lex r (a :: l1) (a :: l2) эквивалентно Lex r l1 l2.

LaTeX

$$$\\mathrm{Lex}\\ r\\ (a::l_1)\ (a::l_2) \\iff \\mathrm{Lex}\\ r\\ l_1\\ l_2.$$$

Lean4

theorem lex_cons_iff {r : α → α → Prop} [IsIrrefl α r] {a l₁ l₂} : Lex r (a :: l₁) (a :: l₂) ↔ Lex r l₁ l₂ :=
  ⟨fun h => by obtain - | h | h := h; exacts [(irrefl_of r a h).elim, h], Lex.cons⟩

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