Multiset.filterMap as a bundled hom #
[UPSTREAM] candidate: the filterMap analogue of
Multiset.mapAddMonoidHom.
def
Multiset.filterMapAddMonoidHom
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
:
Multiset α →+ Multiset β
Multiset.filterMap as an additive monoid hom.
Equations
- Multiset.filterMapAddMonoidHom f = { toFun := fun (s : Multiset α) => Multiset.filterMap f s, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
Multiset.coe_filterMapAddMonoidHom
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
:
⇑(filterMapAddMonoidHom f) = filterMap f
@[simp]
theorem
Multiset.filterMapAddMonoidHom_apply
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(s : Multiset α)
:
(filterMapAddMonoidHom f) s = filterMap f s