Theorem CategoryTheory.MorphismProperty.hasCardinalLT_ofHoms

Modification history

2025-11-21 18:06
Mathlib/CategoryTheory/MorphismProperty/HasCardinalLT.lean
feat(CategoryTheory): HasCardinalLT for MorphismProperty and ObjectProperty (#31421) …
Added CategoryTheory.MorphismProperty.hasCardinalLT_ofHomsView on Github →