map_filterMap_of_inv — Mathlib

English

The attach of a filtered multisets corresponds to attaching the filtered elements and mapping via the membership predicate.

Русский

Прикрепление attach после фильтрации соответствует прикреплению отфильтрованных элементов и отображению через членство.

LaTeX

$$$(s.\mathrm{attach}).\mathrm{filter} (\lambda a:\{a\,\text{∈ } s\}. p(a)) = (s.\mathrm{filter} p).\mathrm{attach}.\mathrm{map}(\mathrm{Subtype}.map\; id\; (\_))$$$

Lean4

theorem map_filterMap_of_inv (f : α → Option β) (g : β → α) (H : ∀ x : α, (f x).map g = some x) (s : Multiset α) :
    map g (filterMap f s) = s :=
  Quot.inductionOn s fun _ => congr_arg ofList <| List.map_filterMap_of_inv H

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