Theorem CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0

Modification history

2026-04-18 08:20
Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
feat(AlgebraicTopology/SimplicialSet): anodyne extensions (#37321)
Added CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0View on Github →