Theorem CategoryTheory.SmallObject.succStruct_prop_le_propArrow

Modification history

2025-02-15 13:09
Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
feat(CategoryTheory): cardinals that are suitable for the small object argument (#21865) …
Added CategoryTheory.SmallObject.succStruct_prop_le_propArrowView on Github →