Documentation Verification Report

Finite

📁 Source: Mathlib/CategoryTheory/Sites/Finite.lean

Statistics

Metric	Count
Definitions `finite`, `finite`	2
Theorems `instHasIsosFinite`, `mem_finite_iff`, `ofArrows_mem_finite`, `finite_toPrecoverage`, `ofArrows_mem_finite`	5
Total	7

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
`finite` 📖	CompOp	4 math math: `mem_finite_iff`, `ofArrows_mem_finite`, `instHasIsosFinite`, `CategoryTheory.Pretopology.finite_toPrecoverage`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasIsosFinite` 📖	mathematical	—	`HasIsos` `finite`	—	`CategoryTheory.Presieve.uncurry_singleton`
`mem_finite_iff` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings` `finite` `Set.Finite` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Presieve.uncurry`	—	—
`ofArrows_mem_finite` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings` `finite` `CategoryTheory.Presieve.ofArrows`	—	`CategoryTheory.Presieve.uncurry_ofArrows` `Set.finite_range`

CategoryTheory.Pretopology

Definitions

Name	Category	Theorems
`finite` 📖	CompOp	2 math math: `ofArrows_mem_finite`, `finite_toPrecoverage`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_toPrecoverage` 📖	mathematical	—	`toPrecoverage` `finite` `CategoryTheory.Precoverage.finite`	—	—
`ofArrows_mem_finite` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage` `finite` `CategoryTheory.Presieve.ofArrows`	—	`CategoryTheory.Precoverage.ofArrows_mem_finite`

---

← Back to Index