# Documentation

Mathlib.Data.Countable.Defs

# Countable types #

In this file we define a typeclass saying that a given Sort* is countable. 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 this typeclass. More instances can be found in other files.

### Definition and basic properties #

theorem countable_iff_exists_injective (α : Sort u) :
f,
class Countable (α : Sort u) :
• exists_injective_nat' : f,

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

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

Instances
theorem Countable.exists_injective_nat (α : Sort u) [] :
f,
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} [] :

### Operations on Sort*s #

instance instCountablePLift {α : Sort u} [] :
instance Subsingleton.to_countable {α : Sort u} [] :
instance Subtype.countable {α : Sort u} [] {p : αProp} :
Countable { x // p x }
instance Finite.to_countable {α : Sort u} [] :
instance Prop.countable (p : Prop) :
instance Quotient.countable {α : Sort u} [] {r : ααProp} :
instance instCountableQuotient {α : Sort u} [] {s : } :