mathlib3

8d41552f - 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 <urkud@urkud.name>