of_mono_eq_zero

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

English

If a morphism f is mono and equals zero, then X is a zero object.

Русский

Если морфизм f моно и равен нулю, то X — нулевой объект.

LaTeX

$$$(Mono f) \land (f = 0) \Rightarrow IsZero X$$$

Lean4

theorem of_mono_eq_zero {X Y : C} (f : X ⟶ Y) [Mono f] (h : f = 0) : IsZero X :=
  by
  subst h
  apply of_mono_zero X Y

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

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

Разделы

Аффилиация

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