All finite types are small.

That is, any α with [Fintype α] is equivalent to a type in any universe.

ink

instance small_of_fintype (α : Type v) [inst : Fintype α] : Small α

Equations

• small_of_fintype = small_of_fintype.proof_1