Documentation Verification Report

Countable

📁 Source: Mathlib/CategoryTheory/Countable.lean

Statistics

Metric	Count
Definitions `CountableCategory`, `HomAsType`, `ObjAsType`, `homAsTypeEquiv`, `instSmallCategoryHomAsType`, `objAsTypeEquiv`	6
Theorems `countableHom`, `countableObj`, `instCountableHomAsType`, `instCountableHomHomAsType`, `instCountableHomObjAsType`, `instCountableObjAsType`, `instHomAsType`, `instLocallySmallObjAsType`, `instObjAsType`, `countableCategoryDiscreteOfCountable`, `countableCategoryOpposite`, `countableCategoryUlift`, `discreteCountable`, `instCountableCategoryNat`, `instCountableCategoryOfCountableOfIsThin`, `instCountableCategoryOfFinCategory`	16
Total	22

CategoryTheory

Definitions

Name	Category	Theorems
`CountableCategory` 📖	CompData	8 math math: `CountableCategory.instObjAsType`, `countableCategoryOpposite`, `instCountableCategoryOfFinCategory`, `instCountableCategoryOfCountableOfIsThin`, `countableCategoryDiscreteOfCountable`, `instCountableCategoryNat`, `countableCategoryUlift`, `CountableCategory.instHomAsType`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countableCategoryDiscreteOfCountable` 📖	mathematical	—	`CountableCategory` `Discrete` `discreteCategory`	—	`discreteCountable` `Finite.to_countable` `Finite.of_fintype`
`countableCategoryOpposite` 📖	mathematical	—	`CountableCategory` `Opposite` `Category.opposite`	—	`Countable.of_equiv` `CountableCategory.countableObj` `CountableCategory.countableHom`
`countableCategoryUlift` 📖	mathematical	—	`CountableCategory` `ULiftHom` `ULiftHom.category` `uliftCategory`	—	`instCountableULift` `CountableCategory.countableObj` `CountableCategory.countableHom`
`discreteCountable` 📖	mathematical	—	`Countable` `Discrete`	—	`Countable.of_equiv`
`instCountableCategoryNat` 📖	mathematical	—	`CountableCategory` `Preorder.smallCategory` `Nat.instPreorder`	—	`instCountableNat` `CountableCategory.countableHom` `instCountableCategoryOfCountableOfIsThin` `Preorder.subsingleton_hom`
`instCountableCategoryOfCountableOfIsThin` 📖	mathematical	`Quiver.IsThin` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	`CountableCategory`	—	—
`instCountableCategoryOfFinCategory` 📖	mathematical	—	`CountableCategory`	—	`Finite.to_countable` `Finite.of_fintype`

CategoryTheory.CountableCategory

Definitions

Name	Category	Theorems
`HomAsType` 📖	CompOp	3 math math: `instCountableHomHomAsType`, `instCountableHomAsType`, `instHomAsType`
`ObjAsType` 📖	CompOp	4 math math: `instObjAsType`, `instLocallySmallObjAsType`, `instCountableHomObjAsType`, `instCountableObjAsType`
`homAsTypeEquiv` 📖	CompOp	—
`instSmallCategoryHomAsType` 📖	CompOp	2 math math: `instCountableHomHomAsType`, `instHomAsType`
`objAsTypeEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countableHom` 📖	mathematical	—	`Countable` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`countableObj` 📖	mathematical	—	`Countable`	—	—
`instCountableHomAsType` 📖	mathematical	—	`Countable` `HomAsType`	—	`Countable.of_equiv` `countableObj` `Countable.toSmall`
`instCountableHomHomAsType` 📖	mathematical	—	`Countable` `Quiver.Hom` `HomAsType` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instSmallCategoryHomAsType`	—	`Countable.of_equiv` `instLocallySmallObjAsType` `instCountableHomObjAsType` `CategoryTheory.Equivalence.full_inverse` `CategoryTheory.Equivalence.faithful_inverse`
`instCountableHomObjAsType` 📖	mathematical	—	`Countable` `Quiver.Hom` `ObjAsType` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.InducedCategory.instCategory` `Shrink` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink`	—	`Countable.of_equiv` `countableHom`
`instCountableObjAsType` 📖	mathematical	—	`Countable` `ObjAsType`	—	`Countable.of_equiv` `countableObj` `Countable.toSmall`
`instHomAsType` 📖	mathematical	—	`CategoryTheory.CountableCategory` `HomAsType` `instSmallCategoryHomAsType`	—	`instCountableHomAsType` `instCountableHomHomAsType`
`instLocallySmallObjAsType` 📖	mathematical	—	`CategoryTheory.LocallySmall` `ObjAsType` `CategoryTheory.InducedCategory.instCategory` `Shrink` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink`	—	`Countable.toSmall` `instCountableHomObjAsType`
`instObjAsType` 📖	mathematical	—	`CategoryTheory.CountableCategory` `ObjAsType` `CategoryTheory.InducedCategory.instCategory` `Shrink` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink`	—	`instCountableObjAsType` `instCountableHomObjAsType`

---

← Back to Index