Commit 2024-02-23 22:33 64d2ea85

View on Github →

feat: push forward FinallySmall along a final functor (#10894)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/FinallySmall.lean

added theorem CategoryTheory.finallySmall_of_final_of_essentiallySmall

added theorem CategoryTheory.finallySmall_of_final_of_finallySmall

added theorem CategoryTheory.initiallySmall_of_initial_of_essentiallySmall

added theorem CategoryTheory.initiallySmall_of_initial_of_initiallySmall