mathlib documentation

data.countable.small

All countable types are small. #

That is, any countable type is equivalent to a type in any universe.

@[protected, instance]
def small_of_countable (α : Type v) [countable α] :