All countable types are small.

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

ink

instance small_of_countable (α : Type v) [inst : Countable α] : Small α

Equations

• small_of_countable = small_of_countable.proof_1