instSubsingleton — Mathlib

English

In the presence of zero morphisms, HasZeroMorphisms C is a subsingleton; there is at most one zero morphism between any pair of objects.

Русский

При наличии нулевых морфизмов HasZeroMorphisms C есть пододнозначность: между любыми двумя объектами существует не более одного нулевого морфизма.

LaTeX

$$$$\\mathrm{Subsingleton}(\\mathrm{HasZeroMorphisms}\\; C).$$$$

Lean4

instance : Subsingleton (HasZeroMorphisms C) :=
  ⟨ext⟩

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