instEpiπ

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

English

For all b,c, Pi.ι f b ≫ Pi.π f c equals if b=c then eqToHom (congrArg f h) else 0.

Русский

Для любых b,c композиция Pi.ι f b ≫ Pi.π f c равна if b=c then eqToHom (congrArg f h) else 0.

LaTeX

$$Pi.ι f b ≫ Pi.π f c = if h : b = c then eqToHom (congrArg f h) else 0$$

Lean4

instance (b : β) : Epi (Sigma.π f b) where left_cancellation _ _ e := by simpa using congrArg (Sigma.ι f b ≫ ·) e

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

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

Разделы

Аффилиация

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