fromListIsChain_cons — Mathlib

English

If l is a nonempty chain and x is connected to l.head, then fromListIsChain (x :: l) equals the cons of fromListIsChain l with x.

Русский

Если l — не пустая цепь и x связана с головой l, то fromListIsChain (x :: l) равен cons из fromListIsChain l с x.

LaTeX

$$$ fromListIsChain (List.cons x l) = (fromListIsChain l l_ne_nil hl).cons x hx $$$

Lean4

theorem fromListIsChain_cons (l : List α) (l_ne_nil : l ≠ []) (hl : l.IsChain (· ~[r] ·)) (x : α)
    (hx : x ~[r] l.head l_ne_nil) :
    fromListIsChain (x :: l) (by simp) (hl.cons_of_ne_nil l_ne_nil hx) =
      (fromListIsChain l l_ne_nil hl).cons x (by simpa) :=
  by
  apply toList_injective
  simp

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