mk_surjective

Mathlib.Logic.Function.Coequalizer

URI: https://scilib.ai/kg/mathlib#Function.Coequalizer.mk_surjective

English

The mk construction from a coequalizer is surjective: mk f g is surjective.

Русский

Коэквализаторная конструкция mk f g сюръективна.

LaTeX

$$$ \operatorname{Function.Coequalizer}.mk f g \;\text{ is surjective}$$$

Lean4

theorem mk_surjective : Function.Surjective (mk f g) :=
  Quot.exists_rep

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru