Documentation
Mathlib
.
Data
.
Countable
.
Small
Search
return to top
source
Imports
Init
Mathlib.Data.Countable.Defs
Mathlib.Logic.Small.Basic
Imported by
Countable
.
toSmall
All countable types are small.
#
That is, any countable type is equivalent to a type in any universe.
source
@[instance 100]
instance
Countable
.
toSmall
(α :
Type
v)
[
Countable
α
]
:
Small.{w, v}
α