Theorem CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrow

Modification history

2025-01-21 18:15
Mathlib/CategoryTheory/Comma/CardinalArrow.lean
feat(CategoryTheory): `Arrow A` is finite iff `A` is a finite category (#19945) …
Added CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrowView on Github →