English
For f : M →* N and g : M' →* N', the kernel of the product map equals the product of kernels: mker (prodMap f g) = (mker f).prod (mker g).
Русский
Для f : M →* N и g : M' →* N' ядро произведения равняется произведению ядер: mker(prodMap f g) = (mker f).prod (mker g).
LaTeX
$$$$ \\mathrm{mker}(\\mathrm{prodMap}\; f\; g) = (\\mathrm{mker}\; f).\\mathrm{prod}(\\mathrm{mker}\; g) $$$$
Lean4
/-- The image under a monoid hom of the submonoid generated by a set equals the submonoid generated
by the image of the set. -/
@[to_additive /-- The image under an `AddMonoid` hom of the `AddSubmonoid` generated by a set equals
the `AddSubmonoid` generated by the image of the set. -/
]
theorem map_mclosure (f : F) (s : Set M) : (closure s).map f = closure (f '' s) :=
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Submonoid.gi N).gc (Submonoid.gi M).gc fun _ ↦ rfl
