destutter'_of_isChain_cons — Mathlib

English

If (a :: l) is a chain, then l.destutter' R a = a :: l.

Русский

Если (a :: l) образует цепочку, то l.destutter' R a = a :: l.

LaTeX

$$$$(a :: l).IsChain\,R \Rightarrow l.destutter'\,R\,a = a :: l.$$$$

Lean4

theorem destutter'_of_isChain_cons (h : (a :: l).IsChain R) : l.destutter' R a = a :: l := by
  induction l generalizing a with
  | nil => simp
  | cons b l hb =>
    obtain ⟨h, hc⟩ := isChain_cons_cons.mp h
    rw [l.destutter'_cons_pos h, hb hc]

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