erase_orderedInsert_of_notMem — Mathlib

English

If x is not a member of xs, erasing after orderedInsert leaves xs unchanged.

Русский

Если x не принадлежит xs, то после orderedInsert x теряет значение, при этом xs остаётся неизменным.

LaTeX

$$$$ a priori\; (x \notin xs) \Rightarrow (xs.orderedInsert(r,x,xs)).erase x = xs. $$$$

Lean4

/-- Inserting then erasing an element that is absent is the identity. -/
theorem erase_orderedInsert_of_notMem [DecidableEq α] {x : α} {xs : List α} (hx : x ∉ xs) :
    (xs.orderedInsert r x).erase x = xs :=
  by
  rw [orderedInsert_eq_take_drop, erase_append_right, List.erase_cons_head, takeWhile_append_dropWhile]
  exact mt ((takeWhile_prefix _).sublist.subset ·) hx

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