Documentation

Mathlib.Data.Countable.Basic

Countable types #

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

instance instCountableInt :

Equations

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 : α ↪ β) :

Operations on `Type*`s #

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

Countable (α ⊕ β)

Equations

(_ : Countable (α ⊕ β)) = (_ : Countable (α ⊕ β))

instance instCountableOption {α : Type u} [Countable α] :

Countable (Option α)

Equations

(_ : Countable (Option α)) = (_ : Countable (Option α))

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

Countable (α × β)

Equations

(_ : Countable (α × β)) = (_ : Countable (α × β))

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

Countable (Sigma π)

Equations

(_ : Countable (Sigma π)) = (_ : Countable (Sigma π))

Operations on `Sort*`s #

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

Equations

(_ : Countable ↑s) = (_ : Countable { x : α // x ∈ s })

instance instCountablePSum {α : Sort u} {β : Sort v} [Countable α] [Countable β] :

Countable (α ⊕' β)

Equations

(_ : Countable (α ⊕' β)) = (_ : Countable (α ⊕' β))

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

Countable (PProd α β)

Equations

(_ : Countable (PProd α β)) = (_ : Countable (PProd α β))

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

Countable (PSigma π)

Equations

(_ : Countable (PSigma π)) = (_ : Countable (PSigma π))

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

Countable ((a : α) → π a)

Equations

(_ : Countable ((a : α) → π a)) = (_ : Countable ((a : α) → π a))