instMonoInr

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

English

The morphism prod.inr X Y is mono; i.e., it is left-cancellable: if m ≫ prod.inr = n ≫ prod.inr then m = n.

Русский

Морфизм prod.inr X Y моно; т. е. лево-отменим.

LaTeX

$$Mono (prod.inr X Y)$$

Lean4

instance : Mono (prod.inr X Y) where right_cancellation _ _ e := by simpa using congrArg (· ≫ prod.snd) e

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

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

Разделы

Аффилиация

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