Theorem CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ιObj

Modification history

2025-02-15 18:13
Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
feat(CategoryTheory/SmallObject): the functorial factorization (#21911) …
Added CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ιObjView on Github →