cons_of_ne_nil — Mathlib

English

If l is nonempty and IsChain R l holds, and R x (l.head l_ne_nil) holds, then the list x :: l is an IsChain R.

Русский

Если l не пуст, IsChain R l выполняется и R x (l.head l_ne_nil) выполняется, тогда x :: l образует IsChain R.

LaTeX

$$l ≠ [] → IsChain R l → R x (l.head l_ne_nil) → IsChain R (List.cons x l)$$

Lean4

theorem cons_of_ne_nil {x : α} {l : List α} (l_ne_nil : l ≠ []) (hl : IsChain R l) (h : R x (l.head l_ne_nil)) :
    IsChain R (x :: l) := by
  refine hl.cons' fun y hy ↦ ?_
  convert h
  simpa [l.head?_eq_head l_ne_nil] using hy.symm

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