Documentation

Mathlib.Data.Countable.Basic

Countable types #

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

Definition in terms of Function.Embedding #

theorem nonempty_embedding_nat (α : Sort u_1) [inst : Countable α] :
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
instance instCountableProd {α : Type u} {β : Type v} [inst : Countable α] [inst : Countable β] :
Countable (α × β)
Equations
instance instCountableSigma {α : Type u} {π : αType w} [inst : Countable α] [inst : ∀ (a : α), Countable (π a)] :
Equations

Operations on Sort _s #

instance SetCoe.countable {α : Type u_1} [inst : Countable α] (s : Set α) :
Equations
instance instCountablePSum {α : Sort u} {β : Sort v} [inst : Countable α] [inst : Countable β] :
Countable (α ⊕' β)
Equations
instance instCountablePProd {α : Sort u} {β : Sort v} [inst : Countable α] [inst : Countable β] :
Equations
instance instCountablePSigma {α : Sort u} {π : αSort w} [inst : Countable α] [inst : ∀ (a : α), Countable (π a)] :
Equations
instance instCountableForAll {α : Sort u} {π : αSort w} [inst : Finite α] [inst : ∀ (a : α), Countable (π a)] :
Countable ((a : α) → π a)
Equations