Countable types

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

theorem instCountableInt : Countable ℤ

Definition in terms of Function.Embedding

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

theorem uncountable_iff_isEmpty_embedding {α : Sort u} : Uncountable α ↔ IsEmpty (α ↪ ℕ)

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

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

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

Operations on Type*s

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

theorem Sum.uncountable_inl {α : Type u} {β : Type v} [Uncountable α] : Uncountable (α ⊕ β)

theorem Sum.uncountable_inr {α : Type u} {β : Type v} [Uncountable β] : Uncountable (α ⊕ β)

theorem Option.instCountable {α : Type u} [Countable α] : Countable (Option α)

theorem WithTop.instCountable {α : Type u} [Countable α] : Countable (WithTop α)

theorem WithBot.instCountable {α : Type u} [Countable α] : Countable (WithBot α)

theorem ENat.instCountable : Countable ℕ∞

theorem Option.instUncountable {α : Type u} [Uncountable α] : Uncountable (Option α)

theorem WithTop.instUncountable {α : Type u} [Uncountable α] : Uncountable (WithTop α)

theorem WithBot.instUncountable {α : Type u} [Uncountable α] : Uncountable (WithBot α)

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

theorem instUncountableProdOfNonempty {α : Type u} {β : Type v} [Uncountable α] [Nonempty β] : Uncountable (α × β)

theorem instUncountableProdOfNonempty_1 {α : Type u} {β : Type v} [Nonempty α] [Uncountable β] : Uncountable (α × β)

theorem countable_left_of_prod_of_nonempty {α : Type u} {β : Type v} [Nonempty β] (h : Countable (α × β)) : Countable α

theorem countable_right_of_prod_of_nonempty {α : Type u} {β : Type v} [Nonempty α] (h : Countable (α × β)) : Countable β

theorem countable_prod_swap {α : Type u} {β : Type v} [Countable (α × β)] : Countable (β × α)

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

theorem Sigma.uncountable {α : Type u} {π : α → Type w} (a : α) [Uncountable (π a)] : Uncountable (Sigma π)

theorem instUncountableSigmaOfNonempty {α : Type u} {π : α → Type w} [Nonempty α] [∀ (a : α), Uncountable (π a)] : Uncountable (Sigma π)

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

Operations on Sort*s

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

theorem instCountablePProd {α : Sort u} {β : Sort v} [Countable α] [Countable β] : Countable (α ×' β)

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

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