map_erase_of_mem — Mathlib

English

If x ∈ s, then (s.erase x).map f = (s.map f).erase (f x).

Русский

Если x ∈ s, то (s.erase x).map f = (s.map f).erase (f x).

LaTeX

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

Lean4

theorem map_erase_of_mem [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) {x : α} (h : x ∈ s) :
    (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 => ?_
  rcases eq_or_ne y x with rfl | hxy
  · simp
  replace h : x ∈ s := by simpa [hxy.symm] using h
  rw [s.erase_cons_tail hxy, map_cons, map_cons, ih h, erase_cons_tail_of_mem (mem_map_of_mem f h)]

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