head!_le_of_lt — Mathlib

English

If l' < l in lex order and l' ≠ empty, then head!(l') ≤ head!(l).

Русский

Если l' < l в лексикографическом порядке и l' ≠ пустой, то head!(l') ≤ head!(l).

LaTeX

$$$(l' < l) \\land (l' \\neq \\emptyset) \\Rightarrow l'.head! \\le l.head!.$$$

Lean4

theorem head!_le_of_lt [Preorder α] [Inhabited α] (l l' : List α) (h : l' < l) (hl' : l' ≠ []) : l'.head! ≤ l.head! :=
  by
  replace h : List.Lex (· < ·) l' l := h
  by_cases hl : l = []
  · simp [hl] at h
  · rw [← List.cons_head!_tail hl', ← List.cons_head!_tail hl] at h
    exact head_le_of_lt h

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