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 Function.Embedding.countable {α : Sort u} {β : Sort v} [Countable β] (f : α β) :
theorem Function.Embedding.uncountable {α : Sort u} {β : Sort v} [Uncountable α] (f : α β) :

Operations on Type*s #

instance instCountableSum {α : Type u} {β : Type v} [Countable α] [Countable β] :
Countable (α β)
Equations
instance Sum.uncountable_inl {α : Type u} {β : Type v} [Uncountable α] :
Equations
instance Sum.uncountable_inr {α : Type u} {β : Type v} [Uncountable β] :
Equations
instance instCountableOption {α : Type u} [Countable α] :
Equations
Equations
instance instCountableProd {α : Type u} {β : Type v} [Countable α] [Countable β] :
Countable (α × β)
Equations
instance instUncountableProd {α : Type u} {β : Type v} [Uncountable α] [Nonempty β] :
Uncountable (α × β)
Equations
instance instUncountableProd_1 {α : Type u} {β : Type v} [Nonempty α] [Uncountable β] :
Uncountable (α × β)
Equations
instance instCountableSigma {α : Type u} {π : αType w} [Countable α] [∀ (a : α), Countable (π a)] :
Equations
theorem Sigma.uncountable {α : Type u} {π : αType w} (a : α) [Uncountable (π a)] :
instance instUncountableSigma {α : Type u} {π : αType w} [Nonempty α] [∀ (a : α), Uncountable (π a)] :
Equations
instance SetCoe.countable {α : Type u} [Countable α] (s : Set α) :
Equations

Operations on Sort*s #

instance instCountablePSum {α : Sort u} {β : Sort v} [Countable α] [Countable β] :
Countable (α ⊕' β)
Equations
instance instCountablePProd {α : Sort u} {β : Sort v} [Countable α] [Countable β] :
Equations
instance instCountablePSigma {α : Sort u} {π : αSort w} [Countable α] [∀ (a : α), Countable (π a)] :
Equations
instance instCountableForAll {α : Sort u} {π : αSort w} [Finite α] [∀ (a : α), Countable (π a)] :
Countable ((a : α) → π a)
Equations