mrange_mk — Mathlib

English

The image (range) of the canonical mk map is the whole coproduct; the submonoid generated by all mk(M) and mk(N) equals the entire CoprodI M N.

Русский

Образ канонического отображения mk есть вся копродукт; подгномоид, порождаемый всеми изображениями из M и N, равен всему CoprodI M N.

LaTeX

$$$ \\mathrm{mrange}(\\mathrm{Monoid.Coprod.mk}) = \\top$$$

Lean4

@[to_additive (attr := simp)]
theorem mrange_mk : MonoidHom.mrange (@mk M N _ _) = ⊤ :=
  Con.mrange_mk'

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