head_le_of_lt — Mathlib

English

If (a' :: l') < (a :: l) in the list lexicographic order, then a' ≤ a in the ambient preorder.

Русский

Если список с головой a' меньше списка с головой a по лексикографическому порядку, то a' ≤ a в исходном порядке.

LaTeX

$$$(a' :: l') < (a :: l) \\Rightarrow a' \\le a.$$$

Lean4

theorem head_le_of_lt [Preorder α] {a a' : α} {l l' : List α} (h : (a' :: l') < (a :: l)) : a' ≤ a :=
  match h with
  | .cons _ => le_rfl
  | .rel h => h.le

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