All countable types are small. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
That is, any countable type is equivalent to a type in any universe.
data.countable.small
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
That is, any countable type is equivalent to a type in any universe.