Documentation Verification Report

Countable

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Countable.lean

Statistics

Metric	Count
Definitions `HasCountableColimits`, `HasCountableCoproducts`, `HasCountableLimits`, `HasCountableProducts`, `sequentialFunctor`, `sequentialFunctor_obj`, `sequentialFunctor`, `sequentialFunctor_obj`	8
Theorems `out`, `out`, `out`, `out`, `sequentialFunctor_initial`, `sequentialFunctor_initial_aux`, `sequentialFunctor_map`, `sequentialFunctor_final`, `sequentialFunctor_final_aux`, `sequentialFunctor_map`, `hasCountableColimits_of_hasColimits`, `hasCountableCoproducts_of_hasCoproducts`, `hasCountableCoproducts_of_hasCountableColimits`, `hasCountableLimits_of_hasLimits`, `hasCountableProducts_of_hasCountableLimits`, `hasCountableProducts_of_hasProducts`, `hasFiniteColimits_of_hasCountableColimits`, `hasFiniteCoproducts_of_hasCountableCoproducts`, `hasFiniteLimits_of_hasCountableLimits`, `hasFiniteProducts_of_hasCountableProducts`, `instHasColimitsOfShapeOfHasCountableColimitsOfCountableCategory`, `instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable`, `instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory`, `instHasProductsOfShapeOfHasCountableProductsOfCountable`	24
Total	32

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`HasCountableColimits` 📖	CompData	1 math math: `hasCountableColimits_of_hasColimits`
`HasCountableCoproducts` 📖	CompData	2 math math: `hasCountableCoproducts_of_hasCoproducts`, `hasCountableCoproducts_of_hasCountableColimits`
`HasCountableLimits` 📖	CompData	2 math math: `LightProfinite.instHasCountableLimits`, `hasCountableLimits_of_hasLimits`
`HasCountableProducts` 📖	CompData	2 math math: `hasCountableProducts_of_hasCountableLimits`, `hasCountableProducts_of_hasProducts`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasCountableColimits_of_hasColimits` 📖	mathematical	—	`HasCountableColimits`	—	`hasColimitsOfShapeOfHasColimitsOfSize` `hasSmallestColimitsOfHasColimits`
`hasCountableCoproducts_of_hasCoproducts` 📖	mathematical	`HasCoproducts`	`HasCountableCoproducts`	—	`has_smallest_coproducts_of_hasCoproducts`
`hasCountableCoproducts_of_hasCountableColimits` 📖	mathematical	—	`HasCountableCoproducts`	—	`instHasColimitsOfShapeOfHasCountableColimitsOfCountableCategory` `CategoryTheory.countableCategoryDiscreteOfCountable`
`hasCountableLimits_of_hasLimits` 📖	mathematical	—	`HasCountableLimits`	—	`hasLimitsOfShapeOfHasLimits` `hasSmallestLimitsOfHasLimits`
`hasCountableProducts_of_hasCountableLimits` 📖	mathematical	—	`HasCountableProducts`	—	`instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory` `CategoryTheory.countableCategoryDiscreteOfCountable`
`hasCountableProducts_of_hasProducts` 📖	mathematical	`HasProducts`	`HasCountableProducts`	—	`has_smallest_products_of_hasProducts`
`hasFiniteColimits_of_hasCountableColimits` 📖	mathematical	—	`HasFiniteColimits`	—	`HasCountableColimits.out` `CategoryTheory.instCountableCategoryOfFinCategory`
`hasFiniteCoproducts_of_hasCountableCoproducts` 📖	mathematical	—	`HasFiniteCoproducts`	—	`instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable` `instCountableFin`
`hasFiniteLimits_of_hasCountableLimits` 📖	mathematical	—	`HasFiniteLimits`	—	`HasCountableLimits.out` `CategoryTheory.instCountableCategoryOfFinCategory`
`hasFiniteProducts_of_hasCountableProducts` 📖	mathematical	—	`HasFiniteProducts`	—	`instHasProductsOfShapeOfHasCountableProductsOfCountable` `instCountableFin`
`instHasColimitsOfShapeOfHasCountableColimitsOfCountableCategory` 📖	mathematical	—	`HasColimitsOfShape`	—	`HasCountableColimits.out` `CategoryTheory.CountableCategory.instHomAsType` `hasColimitsOfShape_of_equivalence`
`instHasCoproductsOfShapeOfHasCountableCoproductsOfCountable` 📖	mathematical	—	`HasCoproductsOfShape`	—	`Countable.toSmall` `Countable.of_equiv` `HasCountableCoproducts.out` `hasColimitsOfShape_of_equivalence`
`instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory` 📖	mathematical	—	`HasLimitsOfShape`	—	`HasCountableLimits.out` `CategoryTheory.CountableCategory.instHomAsType` `hasLimitsOfShape_of_equivalence`
`instHasProductsOfShapeOfHasCountableProductsOfCountable` 📖	mathematical	—	`HasProductsOfShape`	—	`Countable.toSmall` `Countable.of_equiv` `HasCountableProducts.out` `hasLimitsOfShape_of_equivalence`

CategoryTheory.Limits.HasCountableColimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape`	—	—

CategoryTheory.Limits.HasCountableCoproducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`CategoryTheory.Limits.HasCoproductsOfShape`	—	—

CategoryTheory.Limits.HasCountableLimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape`	—	—

CategoryTheory.Limits.HasCountableProducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`CategoryTheory.Limits.HasProductsOfShape`	—	—

CategoryTheory.Limits.IsCofiltered

Definitions

Name	Category	Theorems
`sequentialFunctor` 📖	CompOp	2 math math: `sequentialFunctor_initial`, `LightProfinite.lightToProfinite_map_proj_eq`
`sequentialFunctor_obj` 📖	CompOp	2 math math: `sequentialFunctor_initial_aux`, `sequentialFunctor_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sequentialFunctor_initial` 📖	mathematical	—	`CategoryTheory.Functor.Initial` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `Nat.instPreorder` `sequentialFunctor`	—	`sequentialFunctor_initial_aux` `CategoryTheory.isConnected_of_zigzag` `le_of_lt`
`sequentialFunctor_initial_aux` 📖	mathematical	—	`Preorder.toLE` `sequentialFunctor_obj`	—	`exists_surjective_nat` `CategoryTheory.IsCofiltered.nonempty` `CategoryTheory.IsCofilteredOrEmpty.cone_objs` `CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty` `CategoryTheory.leOfHom`
`sequentialFunctor_map` 📖	mathematical	—	`Antitone` `Nat.instPreorder` `sequentialFunctor_obj`	—	`antitone_nat_of_succ_le` `CategoryTheory.leOfHom` `exists_surjective_nat` `CategoryTheory.IsCofiltered.nonempty` `CategoryTheory.IsCofilteredOrEmpty.cone_objs` `CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty`

CategoryTheory.Limits.IsFiltered

Definitions

Name	Category	Theorems
`sequentialFunctor` 📖	CompOp	1 math math: `sequentialFunctor_final`
`sequentialFunctor_obj` 📖	CompOp	2 math math: `sequentialFunctor_map`, `sequentialFunctor_final_aux`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sequentialFunctor_final` 📖	mathematical	—	`CategoryTheory.Functor.Final` `Preorder.smallCategory` `Nat.instPreorder` `sequentialFunctor`	—	`sequentialFunctor_final_aux` `CategoryTheory.isConnected_of_zigzag` `le_of_lt`
`sequentialFunctor_final_aux` 📖	mathematical	—	`Preorder.toLE` `sequentialFunctor_obj`	—	`exists_surjective_nat` `CategoryTheory.IsFiltered.nonempty` `CategoryTheory.IsFilteredOrEmpty.cocone_objs` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `CategoryTheory.leOfHom`
`sequentialFunctor_map` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `sequentialFunctor_obj`	—	`monotone_nat_of_le_succ` `CategoryTheory.leOfHom` `exists_surjective_nat` `CategoryTheory.IsFiltered.nonempty` `CategoryTheory.IsFilteredOrEmpty.cocone_objs` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty`

---

← Back to Index