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 Option.instCountable {α : Type u} [Countable α] :
Equations
  • =
Equations
  • =
Equations
  • =
Equations
  • =
Equations
  • =
Equations
  • =
instance instCountableProd {α : Type u} {β : Type v} [Countable α] [Countable β] :
Countable (α × β)
Equations
  • =
instance instUncountableProdOfNonempty {α : Type u} {β : Type v} [Uncountable α] [Nonempty β] :
Uncountable (α × β)
Equations
  • =
instance instUncountableProdOfNonempty_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 instUncountableSigmaOfNonempty {α : Type u} {π : αType w} [Nonempty α] [∀ (a : α), Uncountable (π a)] :
Equations
  • =
@[instance 500]
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 β] :
Countable (α ×' β)
Equations
  • =
instance instCountablePSigma {α : Sort u} {π : αSort w} [Countable α] [∀ (a : α), Countable (π a)] :
Equations
  • =
instance instCountableForallOfFinite {α : Sort u} {π : αSort w} [Finite α] [∀ (a : α), Countable (π a)] :
Countable ((a : α) → π a)
Equations
  • =