Commit 2025-01-21 18:15 9db65959

View on Github →

feat(CategoryTheory): Arrow A is finite iff A is a finite category (#19945) We obtain various results about the cardinality of Arrow.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Comma/Arrow.lean

added def CategoryTheory.Arrow.discreteEquiv

added def CategoryTheory.Arrow.equivSigma

added theorem CategoryTheory.Arrow.ext

Created Mathlib/CategoryTheory/Comma/CardinalArrow.lean

added theorem CategoryTheory.Arrow.finite_iff

added def CategoryTheory.Arrow.opEquiv

added theorem CategoryTheory.hasCardinalLT_arrow_discrete_iff

added theorem CategoryTheory.hasCardinalLT_arrow_op_iff

added theorem CategoryTheory.hasCardinalLT_arrow_shrinkHoms_iff

added theorem CategoryTheory.hasCardinalLT_arrow_shrink_iff

added theorem CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrow

added theorem CategoryTheory.locallySmall_of_small_arrow

added theorem CategoryTheory.small_of_small_arrow

Modified Mathlib/CategoryTheory/EssentiallySmall.lean