filterMap_cons_some — Mathlib

English

If f(a) = some b, then filterMap f on the multiset obtained by prepending a to s yields b prepended to filterMap f s.

Русский

Если f(a) = some b, то filterMap f (a :: s) = b :: filterMap f s.

LaTeX

$$$f\,a = \text{some } b \Rightarrow \operatorname{filterMap} f (a \u0026 s) = b \u0026 \operatorname{filterMap} f s$$$

Lean4

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

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