mk_surjective — Mathlib

English

Every associate class has a representative in M; i.e., mk is surjective.

Русский

Любой класс ассоциированности имеет представителя в M; то есть отображение mk сюръективно.

LaTeX

$$$ \forall y : \operatorname{Associates}(M), \exists a : M, \operatorname{Associates.mk} a = y $$$

Lean4

theorem mk_surjective [Monoid M] : Function.Surjective (@Associates.mk M _) :=
  forall_associated.2 fun a => ⟨a, rfl⟩

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