# Documentation

Mathlib.Data.Countable.Small

# All countable types are small. #

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

instance small_of_countable (α : Type v) [inst : ] :
Equations