instSubsingleton — Mathlib

English

If α is a subsingleton, then the discrete category on α is subsingleton; for any objects X, Y in Discrete α, the hom-set Hom(X,Y) contains at most one morphism.

Русский

Если α содержит не более чем один элемент, то дискретная категория на α единична: между любыми двумя объектами X, Y существует не более одного морфизма.

LaTeX

$$$\\forall X,Y\\in \\mathrm{Discrete}(\\alpha),\\; |\\mathrm{Hom}_{\\mathrm{Discrete}(\\alpha)}(X,Y)| \\le 1$$$

Lean4

instance [Subsingleton α] : Subsingleton (Discrete α) :=
  ⟨by cat_disch⟩

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