feat(logic/small): The range of a function from a small type is small (#11029)
feat(logic/small): The range of a function from a small type is small (#11029)

That is, you don't actually need an equivalence to build `small α`, a mere function does the trick.



Co-authored-by: Yury G. Kudryashov <2c59405d0ec2e119a1c3d2318bdb4a6ce50051ae@urkud.name>

leanprover-community/mathlib,leanprover-community/mathlib