erase_eq_filter — Mathlib

English

If s is nodup, then erasing a equals filtering out a from s.

Русский

Если s без повторов, то стирание элемента a эквивалентно фильтрации s по неравенству a.

LaTeX

$$$ [DecidableEq\\, \\alpha] (s:\\\u200bs)\\text{Nodup} \\rightarrow s.\\text{erase } a = \\mathrm{filter}(\\cdot \\neq a) s $$$

Lean4

theorem erase_eq_filter [DecidableEq α] (a : α) {s} : Nodup s → s.erase a = Multiset.filter (· ≠ a) s :=
  Quot.induction_on s fun _ d => congr_arg ((↑) : List α → Multiset α) <| by simpa using List.Nodup.erase_eq_filter d a

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