Countable types #

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

instance instCountableInt :
Equations

Definition in terms of Function.Embedding#

theorem nonempty_embedding_nat (α : Sort u_1) [] :
theorem Function.Embedding.countable {α : Sort u} {β : Sort v} [] (f : α β) :
theorem Function.Embedding.uncountable {α : Sort u} {β : Sort v} [] (f : α β) :

Operations on Type*s #

instance instCountableSum {α : Type u} {β : Type v} [] [] :
Countable (α β)
Equations
• =
instance Sum.uncountable_inl {α : Type u} {β : Type v} [] :
Equations
• =
instance Sum.uncountable_inr {α : Type u} {β : Type v} [] :
Equations
• =
instance instCountableOption {α : Type u} [] :
Equations
• =
instance Option.instUncountable {α : Type u} [] :
Equations
• =
instance instCountableProd {α : Type u} {β : Type v} [] [] :
Countable (α × β)
Equations
• =
instance instUncountableProdOfNonempty {α : Type u} {β : Type v} [] [] :
Uncountable (α × β)
Equations
• =
instance instUncountableProdOfNonempty_1 {α : Type u} {β : Type v} [] [] :
Uncountable (α × β)
Equations
• =
instance instCountableSigma {α : Type u} {π : αType w} [] [∀ (a : α), Countable (π a)] :
Equations
• =
theorem Sigma.uncountable {α : Type u} {π : αType w} (a : α) [Uncountable (π a)] :
instance instUncountableSigmaOfNonempty {α : Type u} {π : αType w} [] [∀ (a : α), Uncountable (π a)] :
Equations
• =
@[instance 500]
instance SetCoe.countable {α : Type u} [] (s : Set α) :
Equations
• =

Operations on Sort*s #

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