Commit 2025-11-21 18:06 d5c9558e
View on Github →feat(CategoryTheory): HasCardinalLT for MorphismProperty and ObjectProperty (#31421)
This PR introduces abbreviations to say that the type of objects or morphisms satisfying a certain property is of cardinality < κ.