Documentation

Mathlib.Data.Countable.Small

All countable types are small. #

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

@[instance 100]
instance Countable.toSmall (α : Type v) [Countable α] :
Equations
  • =
@[deprecated Countable.toSmall]

Alias of Countable.toSmall.

Equations
Instances For
    @[deprecated Countable.toSmall]

    Alias of Countable.toSmall.

    Equations
    Instances For