mathlib3

0b6f9ebb - feat(logic/small): The image of a small set is small (#11108)

feat(logic/small): The image of a small set is small (#11108) A followup to #11029. Only realized this could be easily proved once that PR was approved. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>