mathlib documentation

data.countable.basic

Countable types #

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)