erase_attach_map_val — Mathlib

English

For a decidable equality type, removing an element x from the attach of s and then mapping the attached values back to their underlying values matches erasing x from s and then mapping.

Русский

При существованииDecidableEq, удаление элемента x из attach s и последующее отображение обратно к элементам совпадает с удалением x из s и последующим отображением.

LaTeX

$$$\\forall s:\\\\mathrm{Multiset}\\\\ \\alpha,\\\\forall x:{ x\\\\in s },\\\\ \\mathrm{map}\\\\ (\\\\uparrow)\\\\ (s.\\\\attach.\\\\erase x) = s.\\\\erase x.$$$

Lean4

theorem erase_attach_map_val (s : Multiset α) (x : { x // x ∈ s }) : (s.attach.erase x).map (↑) = s.erase x := by
  rw [Multiset.map_erase _ val_injective, attach_map_val]

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