destutter'_sublist — Mathlib

English

For any list l, l.destutter' R a is a sublist of a :: l.

Русский

Для любого списка l, l.destutter' R a является частичным вложением (подсписком) a :: l.

LaTeX

$$$$l\text{.destutter'}\,R\,a \ <+\ a :: l.$$$$

Lean4

theorem destutter'_sublist (a) : l.destutter' R a <+ a :: l := by
  induction l generalizing a with
  | nil => simp
  | cons b l hl =>
    rw [destutter']
    split_ifs
    · exact Sublist.cons₂ a (hl b)
    · exact (hl a).trans ((l.sublist_cons_self b).cons_cons a)

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