scilib documentation

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.

source
@[protected, instance]
def int.countable  :
countable ℤ

Definition in terms of function.embedding #

source
theorem countable_iff_nonempty_embedding {α : Sort u} :
countable α ↔ nonempty (α ↪ ℕ)
source
theorem nonempty_embedding_nat (α : Sort u_1) [countable α] :
nonempty (α ↪ ℕ)
source
@[protected]
theorem function.embedding.countable {α : Sort u} {β : Sort v} [countable β] (f : α ↪ β) :
countable α

Operations on Type*s #

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

Operations on and Sort*s #

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