Documentation

Mathlib.Data.Countable.Small

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} α
source
@[deprecated Countable.toSmall (since := "2024-03-20")]
theorem small_of_countable (α : Type v) [Countable α] :
Small.{w, v} α

Alias of Countable.toSmall.

source
@[deprecated Countable.toSmall (since := "2024-03-20")]
theorem small_of_fintype (α : Type v) [Countable α] :
Small.{w, v} α

Alias of Countable.toSmall.