instEpiFactorThruImage

Mathlib.CategoryTheory.Abelian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.instEpiFactorThruImage

English

For any f, the map Abelian.factorThruImage f is epi.

Русский

Для любого f отображение Abelian.factorThruImage f является эпиморфизмом.

LaTeX

$$$$ \\text{Epi } (Abelian.factorThruImage f) $$$$

Lean4

/-- The map `p : P ⟶ image f` is an epimorphism -/
instance : Epi (Abelian.factorThruImage f) := by infer_instance

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

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

Разделы

Аффилиация

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