epi_desc_of_epi_right

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.biprod.epi_desc_of_epi_right

← MathLib Explorer

English

If g is epi, then biprod.desc f g is epi.

Русский

Если g эпиморфизм, то biprod.desc f g является эпиморфизмом.

LaTeX

$$$\text{If } g \text{ is epi, then } \biprod.desc f g \text{ is epi}$$$

Lean4

instance epi_desc_of_epi_right {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi g] :
    Epi (biprod.desc f g) :=
  epi_of_epi_fac <| biprod.inr_desc _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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