Documentation

Mathlib.Data.Countable.Basic

Countable types #

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

instance instCountableInt :

Equations

instCountableInt = instCountableInt.proof_1

Definition in terms of `Function.Embedding` #

theorem countable_iff_nonempty_embedding {α : Sort u} :

Countable α ↔ Nonempty (α ↪ ℕ)

theorem nonempty_embedding_nat (α : Sort u_1) [inst : Countable α] :

Nonempty (α ↪ ℕ)

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

Operations on `Type _`s #

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

Countable (α ⊕ β)

Equations

@instCountableSum = @instCountableSum.proof_1

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

Countable (Option α)

Equations

@instCountableOption = @instCountableOption.proof_1

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

Countable (α × β)

Equations

@instCountableProd = @instCountableProd.proof_1

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

Countable (Sigma π)

Equations

@instCountableSigma = @instCountableSigma.proof_1

Operations on `Sort _`s #

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

Equations

@SetCoe.countable = @SetCoe.countable.proof_1

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

Countable (α ⊕' β)

Equations

@instCountablePSum = @instCountablePSum.proof_1

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

Countable (PProd α β)

Equations

@instCountablePProd = @instCountablePProd.proof_1

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

Countable (PSigma π)

Equations

@instCountablePSigma = @instCountablePSigma.proof_1

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

Countable ((a : α) → π a)

Equations

@instCountableForAll = @instCountableForAll.proof_1