countableCategoryOpposite — Mathlib

English

The opposite of a countable category is countable.

Русский

Противоположная категория счетной категории счетна.

LaTeX

$$$\operatorname{CountableCategory}(J) \Rightarrow \operatorname{CountableCategory}(J^{\mathrm{op}})$$$

Lean4

/-- The opposite of a countable category is countable. -/
instance countableCategoryOpposite {J : Type*} [Category J] [CountableCategory J] : CountableCategory Jᵒᵖ
    where
  countableObj := Countable.of_equiv _ equivToOpposite
  countableHom j j' := Countable.of_equiv _ (opEquiv j j').symm

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