English
If F is a structure providing a MonoidHomClass α β, then mapMonoidHom φ is a monoid hom from Filter α to Filter β induced by map φ.
Русский
Если имеется структура, задающая MonoidHomClass α β, то mapMonoidHom φ является гомоморфизмом моноида от Filter α к Filter β, индуцируемым map φ.
LaTeX
$$$\text{mapMonoidHom }(\varphi): \mathrm{Filter}(\alpha) \to \mathrm{Filter}(\beta)\quad \text{is a MonoidHom}.$$$
Lean4
/-- If `φ : α →* β` then `mapMonoidHom φ` is the monoid homomorphism
`Filter α →* Filter β` induced by `map φ`. -/
@[to_additive /-- If `φ : α →+ β` then `mapAddMonoidHom φ` is the monoid homomorphism
`Filter α →+ Filter β` induced by `map φ`. -/
]
def mapMonoidHom [MonoidHomClass F α β] (φ : F) : Filter α →* Filter β
where
toFun := map φ
map_one' := Filter.map_one φ
map_mul' _ _ := Filter.map_mul φ
