le_head! — Mathlib

English

If a list is sorted by ≤ and is nodup, then it is sorted by <.

Русский

Если список отсортирован по ≤ и не содержит повторов, то он отсортирован по <.

LaTeX

$$$ h_1:\\ l.\\text{Sorted}(\\le) \\to h_2:\\ l.\\text{Nodup} \\Rightarrow l.\\text{Sorted}(<) $$$

Lean4

theorem le_head! [Inhabited α] [Preorder α] {a : α} {l : List α} (h : Sorted (· > ·) l) (ha : a ∈ l) : a ≤ l.head! :=
  by
  rw [← List.cons_head!_tail (List.ne_nil_of_mem ha)] at h ha
  cases ha
  · exact le_rfl
  · exact le_of_lt (rel_of_sorted_cons h a (by assumption))

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