mk_surjective — Mathlib

English

The canonical injection mk from the pair of monoids (M, N) into their coproduct (CoprodI M N) is surjective; every element of the coproduct arises from some pair via this injection.

Русский

Каноническое отображение mk из пары моноидов (M, N) в их копродукт (CoprodI M N) сюръективно; каждый элемент копродукта получается как образ некоторой пары через это отображение.

LaTeX

$$$ \\mathrm{Surjective}\\big( \\mathrm{Monoid.Coprod.mk} \\big)$$$

Lean4

@[to_additive]
theorem mk_surjective : Surjective (@mk M N _ _) :=
  Quot.mk_surjective

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