# mathlib3documentation

data.countable.basic

# Countable types #

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

In this file we provide basic instances of the countable typeclass defined elsewhere.

@[protected, instance]

### Definition in terms of function.embedding#

theorem nonempty_embedding_nat (α : Sort u_1) [countable α] :
@[protected]
theorem function.embedding.countable {α : Sort u} {β : Sort v} [countable β] (f : α β) :

### Operations on Type*s #

@[protected, instance]
def sum.countable {α : Type u} {β : Type v} [countable α] [countable β] :
countable β)
@[protected, instance]
def option.countable {α : Type u} [countable α] :
@[protected, instance]
def prod.countable {α : Type u} {β : Type v} [countable α] [countable β] :
countable × β)
@[protected, instance]
def sigma.countable {α : Type u} {π : α Type w} [countable α] [ (a : α), countable (π a)] :

### Operations on and Sort*s #

@[protected, instance]
def set_coe.countable {α : Type u_1} [countable α] (s : set α) :
@[protected, instance]
def psum.countable {α : Sort u} {β : Sort v} [countable α] [countable β] :
countable (psum α β)
@[protected, instance]
def pprod.countable {α : Sort u} {β : Sort v} [countable α] [countable β] :
@[protected, instance]
def psigma.countable {α : Sort u} {π : α Sort w} [countable α] [ (a : α), countable (π a)] :
@[protected, instance]
def pi.countable {α : Sort u} {π : α Sort w} [finite α] [ (a : α), countable (π a)] :
countable (Π (a : α), π a)