instCountableObjAsType — Mathlib

English

Let α be a type with a countable category structure; then for i,j in ObjAsType α, the hom-set (i ⟶ j) in the induced category is countable.

Русский

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

LaTeX

$$$ \\operatorname{Countable}\\big(\\mathrm{Hom}_{\\mathrm{InducedCategory}}(i,j)\\big) $$$

Lean4

instance : Countable (ObjAsType α) :=
  Countable.of_equiv α (equivShrink.{0} α)

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