instCountableHomObjAsType — Mathlib

English

For α with a countable category structure, and i,j objects in ObjAsType α, the hom-set (i ⟶ j) in the induced category is countable.

Русский

Пусть α счетна как категория; для i,j в ObjAsType α гомоморфизмы i ⟶ j индуцированной категории счетны.

LaTeX

$$$ {i j : \\mathrm{ObjAsType}(\\alpha)}\\;\\operatorname{Countable}(i \\to j) $$$

Lean4

instance {i j : ObjAsType α} : Countable (i ⟶ j) :=
  CountableCategory.countableHom ((equivShrink.{0} α).symm i) _

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