map_erase — Mathlib

English

Erase x from s and map f equals erase f x from map f s.

Русский

Удаление элемента x из s и отображение через f эквивалентно удалению f(x) из map f s.

LaTeX

$$$$(s.erase x).map f = (s.map f).erase (f x) $$$$

Lean4

theorem map_erase [DecidableEq α] [DecidableEq β] (f : α → β) (hf : Function.Injective f) (x : α) (s : Multiset α) :
    (s.erase x).map f = (s.map f).erase (f x) :=
  by
  induction s using Multiset.induction_on with
  | empty => simp
  | cons y s ih => ?_
  by_cases hxy : y = x
  · cases hxy
    simp
  · rw [s.erase_cons_tail hxy, map_cons, map_cons, (s.map f).erase_cons_tail (hf.ne hxy), ih]

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