erase_orderedInsert — Mathlib

English

For a reflexive relation r, inserting x into xs and then erasing x returns xs.

Русский

При отражающем отношении r вставка x в xs с последующим стиранием x возвращает xs.

LaTeX

$$$$ (\mathrm{orderedInsert}(r,x,xs)).\mathrm{erase}(x) = xs. $$$$

Lean4

/-- For a reflexive relation, insert then erasing is the identity. -/
theorem erase_orderedInsert [DecidableEq α] [IsRefl α r] (x : α) (xs : List α) : (xs.orderedInsert r x).erase x = xs :=
  by
  rw [orderedInsert_eq_take_drop, erase_append_right, List.erase_cons_head, takeWhile_append_dropWhile]
  intro h
  replace h := mem_takeWhile_imp h
  simp [refl x] at h

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