Countable types

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

instance instCountableInt : Countable ℤ

Definition in terms of Function.Embedding

theorem countable_iff_nonempty_embedding {α : Sort u} : Countable α ↔ Nonempty (α ↪ ℕ)

theorem nonempty_embedding_nat (α : Sort u_1) [Countable α] : Nonempty (α ↪ ℕ)

theorem Function.Embedding.countable {α : Sort u} {β : Sort v} [Countable β] (f : α ↪ β) : Countable α

Operations on Type*s

instance instCountableSum {α : Type u} {β : Type v} [Countable α] [Countable β] : Countable (α ⊕ β)

instance instCountableOption {α : Type u} [Countable α] : Countable (Option α)

instance instCountableProd {α : Type u} {β : Type v} [Countable α] [Countable β] : Countable (α × β)

instance instCountableSigma {α : Type u} {π : α → Type w} [Countable α] [∀ (a : α), Countable (π a)] : Countable (Sigma π)

Operations on Sort*s

instance SetCoe.countable {α : Type u_1} [Countable α] (s : Set α) : Countable ↑s

instance instCountablePSum {α : Sort u} {β : Sort v} [Countable α] [Countable β] : Countable (α ⊕' β)

instance instCountablePProd {α : Sort u} {β : Sort v} [Countable α] [Countable β] : Countable (PProd α β)

instance instCountablePSigma {α : Sort u} {π : α → Sort w} [Countable α] [∀ (a : α), Countable (π a)] : Countable (PSigma π)

instance instCountableForAll {α : Sort u} {π : α → Sort w} [Finite α] [∀ (a : α), Countable (π a)] : Countable ((a : α) → π a)