instMonoι_1

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.instMonoι_1

English

For any b, the injection Pi.ι f b is a monomorphism.

Русский

Для любого индекса b инъекция Pi.ι f b является мономорфизмом.

LaTeX

$$Mono (Pi.ι f b)$$

Lean4

instance (b : β) : Mono (Pi.ι f b) where right_cancellation _ _ e := by simpa using congrArg (· ≫ Pi.π f b) e

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

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

Разделы

Аффилиация

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