# 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 #

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) [inst : ] :
f,
instance instCountableNat :
Equations
theorem Function.Injective.countable {α : Sort u} {β : Sort v} [inst : ] {f : αβ} (hf : ) :
theorem Function.Surjective.countable {α : Sort u} {β : Sort v} [inst : ] {f : αβ} (hf : ) :
theorem exists_surjective_nat (α : Sort u) [inst : ] [inst : ] :
f,
theorem countable_iff_exists_surjective {α : Sort u} [inst : ] :
f,
theorem Countable.of_equiv {β : Sort v} (α : Sort u_1) [inst : ] (e : α β) :
theorem Equiv.countable_iff {α : Sort u} {β : Sort v} (e : α β) :
instance instCountableULift {β : Type v} [inst : ] :
Equations

### Operations on Sort _s #

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