Documentation Verification Report

CardinalArrow

📁 Source: Mathlib/CategoryTheory/Comma/CardinalArrow.lean

Statistics

Metric	Count
Definitions `opEquiv`, `shrinkEquiv`, `shrinkHomsEquiv`	3
Theorems `finite`, `finite_iff`, `hasCardinalLT_arrow_discrete_iff`, `hasCardinalLT_arrow_op_iff`, `hasCardinalLT_arrow_shrinkHoms_iff`, `hasCardinalLT_arrow_shrink_iff`, `hasCardinalLT_of_hasCardinalLT_arrow`, `instFiniteArrowDiscrete`, `locallySmall_of_small_arrow`, `small_of_small_arrow`	10
Total	13

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasCardinalLT_arrow_discrete_iff` 📖	mathematical	—	`HasCardinalLT` `Arrow` `Discrete` `discreteCategory`	—	`hasCardinalLT_iff_of_equiv`
`hasCardinalLT_arrow_op_iff` 📖	mathematical	—	`HasCardinalLT` `Arrow` `Opposite` `Category.opposite`	—	`hasCardinalLT_iff_of_equiv`
`hasCardinalLT_arrow_shrinkHoms_iff` 📖	mathematical	—	`HasCardinalLT` `Arrow` `ShrinkHoms` `ShrinkHoms.instCategory`	—	`hasCardinalLT_iff_of_equiv`
`hasCardinalLT_arrow_shrink_iff` 📖	mathematical	—	`HasCardinalLT` `Arrow` `Shrink` `Shrink.instCategoryShrink`	—	`hasCardinalLT_iff_of_equiv`
`hasCardinalLT_of_hasCardinalLT_arrow` 📖	—	`HasCardinalLT` `Arrow`	—	—	`HasCardinalLT.of_injective`
`instFiniteArrowDiscrete` 📖	mathematical	—	`Finite` `Arrow` `Discrete` `discreteCategory`	—	`Finite.of_equiv`
`locallySmall_of_small_arrow` 📖	mathematical	—	`LocallySmall`	—	`small_of_injective`
`small_of_small_arrow` 📖	mathematical	—	`Small`	—	`small_of_injective`

CategoryTheory.Arrow

Definitions

Name	Category	Theorems
`opEquiv` 📖	CompOp	—
`shrinkEquiv` 📖	CompOp	—
`shrinkHomsEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Finite` `CategoryTheory.Arrow`	—	`finite_iff`
`finite_iff` 📖	mathematical	—	`Finite` `CategoryTheory.Arrow` `CategoryTheory.FinCategory`	—	`Finite.of_injective` `Finite.of_fintype`

---

← Back to Index