instIsDiscrete — Mathlib

English

If T is a discrete category, then ShrinkHoms T is discrete.

Русский

Если T дискретная категория, то ShrinkHoms T дискретна.

LaTeX

$$$\operatorname{IsDiscrete}(\mathrm{ShrinkHoms}\, T)$$$

Lean4

instance {T : Type u} [Category.{v} T] [IsDiscrete T] : IsDiscrete (ShrinkHoms.{u} T)
    where
  subsingleton _ _ := { allEq _ _ := Shrink.ext (Subsingleton.elim _ _) }
  eq_of_hom f := IsDiscrete.eq_of_hom (C := T) ((equivShrink _).symm f)

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