# mathlib3documentation

data.countable.defs

# Countable types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
structure countable (α : Sort u) :
Prop

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

Instances of this typeclass
@[protected, instance]
@[protected]
theorem function.injective.countable {α : Sort u} {β : Sort v} [countable β] {f : α β} (hf : function.injective f) :
@[protected]
theorem function.surjective.countable {α : Sort u} {β : Sort v} [countable α] {f : α β} (hf : function.surjective f) :
theorem exists_surjective_nat (α : Sort u) [nonempty α] [countable α] :
(f : α),
theorem countable_iff_exists_surjective {α : Sort u} [nonempty α] :
(f : α),
theorem countable.of_equiv {β : Sort v} (α : Sort u_1) [countable α] (e : α β) :
theorem equiv.countable_iff {α : Sort u} {β : Sort v} (e : α β) :
@[protected, instance]
def ulift.countable {β : Type v} [countable β] :

### Operations on Sort*s #

@[protected, instance]
def plift.countable {α : Sort u} [countable α] :
@[protected, instance]
@[protected, instance]
def subtype.countable {α : Sort u} [countable α] {p : α Prop} :
countable {x // p x}
@[protected, instance]
def fin.countable {n : } :
@[protected, instance]
def finite.to_countable {α : Sort u} [finite α] :
@[protected, instance]
@[protected, nolint, instance]
def Prop.countable (p : Prop) :
@[protected, instance]
@[protected, instance]
def Prop.countable'  :
@[protected, instance]
def quot.countable {α : Sort u} [countable α] {r : α α Prop} :
countable (quot r)
@[protected, instance]
def quotient.countable {α : Sort u} [countable α] {s : setoid α} :