English
For a monoid hom f: α →* β and a SetSemiring α, the image of the set s under f, transported to the SetSemiring on β, equals imageHom f s.
Русский
Для гомоморфа моноидов f: α →* β и множества SetSemiring α образ множества s под действием f, приведённый к структуре SetSemiring β, совпадает с imageHom f s.
LaTeX
$$$\\mathrm{imageHom}\: f\\: s = (\\mathrm{image}\: f\\: s.\\down).\\up$$$
Lean4
theorem imageHom_def [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
imageHom f s = (image f s.down).up :=
rfl