Mathlib.Data.Countable.Small

Module docstring

{"# All countable types are small.

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

Countable.toSmall instance

(α : Type v) [Countable α] : Small.{w} α

Full source

instance (priority := 100) Countable.toSmall (α : Type v) [Countable α] : Small.{w} α :=
  let ⟨_, hf⟩ := exists_injective_nat α
  small_of_injective hf

Countable Types are Small

Informal description

For any countable type $\alpha$, $\alpha$ is $w$-small (i.e., there exists a bijection between $\alpha$ and some type in the universe `Type w`).

Uncountable.of_not_small theorem

{α : Type v} (h : ¬Small.{w} α) : Uncountable α

Full source

theorem Uncountable.of_not_small {α : Type v} (h : ¬ Small.{w} α) : Uncountable α := by
  rw [uncountable_iff_not_countable]
  exact mt (@Countable.toSmall α) h

Non-small types are uncountable

Informal description

If a type $\alpha$ is not $w$-small (i.e., there is no bijection between $\alpha$ and any type in the universe `Type w`), then $\alpha$ is uncountable.