imageHom_def — Mathlib

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

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