filterMap_cons_none — Mathlib

English

If an element a is mapped to none by f, then adding a to a multiset before applying filterMap f does not change the result.

Русский

Если для некоторого элемента a условие f(a)=none, то добавление a к мультиету до применения filterMap f не изменяет результат.

LaTeX

$$$f\,a = \mathrm{none} \Rightarrow \operatorname{filterMap} f (a \;\u0026\; s) = \operatorname{filterMap} f s$$$

Lean4

@[simp]
theorem filterMap_cons_none {f : α → Option β} (a : α) (s : Multiset α) (h : f a = none) :
    filterMap f (a ::ₘ s) = filterMap f s :=
  Quot.inductionOn s fun _ => congr_arg ofList <| List.filterMap_cons_none h

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