English
Let f: M → N be a semigroup hom and S ⊆ M. Then the image under f of the subsemigroup generated by S equals the subsemigroup generated by the image of S.
Русский
Пусть f: M → N — гомоморфизм полугрупп и S ⊆ M. Образ порождаемой S подгруппы по f равен замыканию образа S: f(closure(S)) = closure(f[S]).
LaTeX
$$$ f(\\operatorname{closure}(S)) = \\operatorname{closure}(f[S]) $$$
Lean4
/-- The image under a semigroup hom of the subsemigroup generated by a set equals the subsemigroup
generated by the image of the set. -/
@[to_additive /-- The image under an `AddSemigroup` hom of the `AddSubsemigroup` generated by a set
equals the `AddSubsemigroup` generated by the image of the set. -/
]
theorem map_mclosure (f : M →ₙ* N) (s : Set M) : (closure s).map f = closure (f '' s) :=
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subsemigroup.gi N).gc (Subsemigroup.gi M).gc fun _ ↦ rfl
