mathlib documentation

data.equiv.encodable.small

All encodable types are small. #

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

source
@[protected, instance]
def small_of_encodable (α : Type v) [encodable α] :
small α