All countable types are small.

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

instance Countable.toSmall (α : Type v) [Countable α] : Small.{w, v} α

Equations

• ⋯ = ⋯

@[deprecated Countable.toSmall]

def small_of_countable (α : Type v) [Countable α] : Small.{w, v} α

Alias of Countable.toSmall.

Equations

• small_of_countable = Countable.toSmall

@[deprecated Countable.toSmall]

def small_of_fintype (α : Type v) [Countable α] : Small.{w, v} α

Alias of Countable.toSmall.

Equations

• small_of_fintype = Countable.toSmall