# Countable and uncountable types #

In this file we define a typeclass Countable saying that a given Sort* is countable and a typeclass Uncountable saying that a given Type* is uncountable.

See also Encodable for a version that singles out a specific encoding of elements of α by natural numbers.

This file also provides a few instances of these typeclasses. More instances can be found in other files.

### Definition and basic properties #

theorem countable_iff_exists_injective (α : Sort u) :
∃ (f : α),
class Countable (α : Sort u) :

A type α is countable if there exists an injective map α → ℕ.

• exists_injective_nat' : ∃ (f : α),

A type α is countable if there exists an injective map α → ℕ.

Instances
theorem Countable.exists_injective_nat (α : Sort u) [] :
∃ (f : α),
instance instCountableNat :
Equations
theorem Function.Injective.countable {α : Sort u} {β : Sort v} [] {f : αβ} (hf : ) :
theorem Function.Surjective.countable {α : Sort u} {β : Sort v} [] {f : αβ} (hf : ) :
theorem exists_surjective_nat (α : Sort u) [] [] :
∃ (f : α),
theorem countable_iff_exists_surjective {α : Sort u} [] :
∃ (f : α),
theorem Countable.of_equiv {β : Sort v} (α : Sort u_1) [] (e : α β) :
theorem Equiv.countable_iff {α : Sort u} {β : Sort v} (e : α β) :
instance instCountableULift {β : Type v} [] :
Equations

### Operations on Sort*s #

instance instCountablePLift {α : Sort u} [] :
Equations
instance Subsingleton.to_countable {α : Sort u} [] :
Equations
• (_ : ) = (_ : )
instance Subtype.countable {α : Sort u} [] {p : αProp} :
Countable { x : α // p x }
Equations
instance instCountableFin {n : } :
Equations
instance Finite.to_countable {α : Sort u} [] :
Equations
• (_ : ) = (_ : )
Equations
instance Prop.countable (p : Prop) :
Equations
• (_ : ) = (_ : )
instance Bool.countable :
Equations
instance Prop.countable' :
Equations
instance Quotient.countable {α : Sort u} [] {r : ααProp} :
Equations
instance instCountableQuotient {α : Sort u} [] {s : } :
Equations

### Uncountable types #

class Uncountable (α : Sort u_1) :

A type α is uncountable if it is not countable.

• not_countable :

A type α is uncountable if it is not countable.

Instances
theorem not_uncountable_iff {α : Sort u} :
theorem not_countable_iff {α : Sort u} :
@[simp]
theorem not_uncountable {α : Sort u} [] :
@[simp]
theorem not_countable {α : Sort u} [] :
theorem Function.Injective.uncountable {α : Sort u} {β : Sort v} [] {f : αβ} (hf : ) :
theorem Function.Surjective.uncountable {α : Sort u} {β : Sort v} [] {f : αβ} (hf : ) :
theorem not_injective_uncountable_countable {α : Sort u} {β : Sort v} [] [] (f : αβ) :
theorem not_surjective_countable_uncountable {α : Sort u} {β : Sort v} [] [] (f : αβ) :
theorem uncountable_iff_forall_not_surjective {α : Sort u} [] :
∀ (f : α),
theorem Uncountable.of_equiv {β : Sort v} (α : Sort u_1) [] (e : α β) :
theorem Equiv.uncountable_iff {α : Sort u} {β : Sort v} (e : α β) :
instance instUncountableULift {β : Type v} [] :
Equations
instance instUncountablePLift {α : Sort u} [] :
Equations
instance instInfinite {α : Sort u} [] :
Equations
• (_ : ) = (_ : )