Documentation

Mathlib.Data.Countable.Defs

Countable and uncountable types #

In this file we define a typeclass Countable saying that a given Sort* is countable and a typeclass Uncountable saying that a given Type* is uncountable.

See also Encodable for a version that singles out a specific encoding of elements of α by natural numbers.

This file also provides a few instances of these typeclasses. More instances can be found in other files.

Definition and basic properties #

class Countable (α : Sort u) :

A type α is countable if there exists an injective map α → ℕ.

  • exists_injective_nat' : ∃ (f : α), Function.Injective f

    A type α is countable if there exists an injective map α → ℕ.

Instances
    theorem Countable.exists_injective_nat (α : Sort u) [Countable α] :
    ∃ (f : α), Function.Injective f
    theorem Function.Injective.countable {α : Sort u} {β : Sort v} [Countable β] {f : αβ} (hf : Function.Injective f) :
    theorem Function.Surjective.countable {α : Sort u} {β : Sort v} [Countable α] {f : αβ} (hf : Function.Surjective f) :
    theorem exists_surjective_nat (α : Sort u) [Nonempty α] [Countable α] :
    ∃ (f : α), Function.Surjective f
    theorem Countable.of_equiv {β : Sort v} (α : Sort u_1) [Countable α] (e : α β) :
    theorem Equiv.countable_iff {α : Sort u} {β : Sort v} (e : α β) :
    Equations

    Operations on Sort*s #

    instance instCountablePLift {α : Sort u} [Countable α] :
    Equations
    Equations
    instance Subtype.countable {α : Sort u} [Countable α] {p : αProp} :
    Countable { x : α // p x }
    Equations
    instance instCountableFin {n : } :
    Equations
    instance Finite.to_countable {α : Sort u} [Finite α] :
    Equations
    instance Prop.countable (p : Prop) :
    Equations
    instance Quotient.countable {α : Sort u} [Countable α] {r : ααProp} :
    Equations
    instance instCountableQuotient {α : Sort u} [Countable α] {s : Setoid α} :
    Equations

    Uncountable types #

    class Uncountable (α : Sort u_1) :

    A type α is uncountable if it is not countable.

    • not_countable : ¬Countable α

      A type α is uncountable if it is not countable.

    Instances
      @[simp]
      theorem not_uncountable {α : Sort u} [Countable α] :
      @[simp]
      theorem not_countable {α : Sort u} [Uncountable α] :
      theorem Function.Injective.uncountable {α : Sort u} {β : Sort v} [Uncountable α] {f : αβ} (hf : Function.Injective f) :
      theorem Function.Surjective.uncountable {α : Sort u} {β : Sort v} [Uncountable β] {f : αβ} (hf : Function.Surjective f) :
      theorem not_injective_uncountable_countable {α : Sort u} {β : Sort v} [Uncountable α] [Countable β] (f : αβ) :
      theorem Uncountable.of_equiv {β : Sort v} (α : Sort u_1) [Uncountable α] (e : α β) :
      theorem Equiv.uncountable_iff {α : Sort u} {β : Sort v} (e : α β) :
      Equations
      instance instInfinite {α : Sort u} [Uncountable α] :
      Equations