English
Given a suitable family of maps f that behave like a monoid homomorphism, one can lift f to a monoid homomorphism from Finset α to Finset β by sending each finite subset to its image under f.
Русский
Пусть имеется подходящее отображение f, сохраняющее умножение подобным образом; тогда существует моноид-гомоморфизм от Finset α к Finset β, отправляющий конечное подмножество s в образ f[s].
LaTeX
$$$\\operatorname{imageMonoidHom}(f) : \\mathrm{Finset}\\,\\alpha \\to^* \\mathrm{Finset}\\,\\beta$, где $\\operatorname{imageMonoidHom}(f)(s) = f[ s ]$ и $1$ отправляется в $1$.$$
Lean4
/-- Lift a `MonoidHom` to `Finset` via `image`. -/
@[to_additive (attr := simps) /-- Lift an `add_monoid_hom` to `Finset` via `image` -/
]
def imageMonoidHom [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] (f : F) : Finset α →* Finset β :=
{ imageMulHom f, imageOneHom f with }
