instEpiπ

Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.kernelCokernelCompSequence.instEpiπ

English

The map π in the kernel-cokernel sequence is onto.

Русский

Отображение π в последовательности ядра–кококernel сюръективно.

LaTeX

$$Epi(π f g)$$

Lean4

instance : Epi (π f g) :=
  epi_of_epi_fac (inr_π f g)

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

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

Разделы

Аффилиация

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