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 #

source
theorem countable_iff_exists_injective (α : Sort u) :
Countable α ↔ ∃ (f : α → ℕ), Function.Injective f
source
class Countable (α : Sort u) :
Prop

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
    source
    theorem Countable.exists_injective_nat' {α : Sort u} [self : Countable α] :
    ∃ (f : α → ℕ), Function.Injective f

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

    source
    theorem Countable.exists_injective_nat (α : Sort u) [Countable α] :
    ∃ (f : α → ℕ), Function.Injective f
    source
    instance instCountableNat :
    Countable ℕ
    Equations
    source
    theorem Function.Injective.countable {α : Sort u} {β : Sort v} [Countable β] {f : α → β} (hf : Function.Injective f) :
    Countable α
    source
    theorem Function.Surjective.countable {α : Sort u} {β : Sort v} [Countable α] {f : α → β} (hf : Function.Surjective f) :
    Countable β
    source
    theorem exists_surjective_nat (α : Sort u) [Nonempty α] [Countable α] :
    ∃ (f : ℕ → α), Function.Surjective f
    source
    theorem countable_iff_exists_surjective {α : Sort u} [Nonempty α] :
    Countable α ↔ ∃ (f : ℕ → α), Function.Surjective f
    source
    theorem Countable.of_equiv {β : Sort v} (α : Sort u_1) [Countable α] (e : α ≃ β) :
    Countable β
    source
    theorem Equiv.countable_iff {α : Sort u} {β : Sort v} (e : α ≃ β) :
    Countable α ↔ Countable β
    source
    instance instCountableULift {β : Type v} [Countable β] :
    Countable (ULift.{u, v} β)
    Equations
    • ⋯ = ⋯

    Operations on Sort*s #

    source
    instance instCountablePLift {α : Sort u} [Countable α] :
    Countable (PLift α)
    Equations
    • ⋯ = ⋯
    source
    @[instance 100]
    instance Subsingleton.to_countable {α : Sort u} [Subsingleton α] :
    Countable α
    Equations
    • ⋯ = ⋯
    source
    @[instance 500]
    instance Subtype.countable {α : Sort u} [Countable α] {p : α → Prop} :
    Countable { x : α // p x }
    Equations
    • ⋯ = ⋯
    source
    instance instCountableFin {n : ℕ} :
    Countable (Fin n)
    Equations
    • ⋯ = ⋯
    source
    @[instance 100]
    instance Finite.to_countable {α : Sort u} [Finite α] :
    Countable α
    Equations
    • ⋯ = ⋯
    source
    instance instCountablePUnit :
    Countable PUnit.{u}
    Equations
    source
    @[instance 100]
    instance Prop.countable (p : Prop) :
    Countable p
    Equations
    • ⋯ = ⋯
    source
    instance Bool.countable :
    Countable Bool
    Equations
    source
    instance Prop.countable' :
    Countable Prop
    Equations
    source
    @[instance 500]
    instance Quotient.countable {α : Sort u} [Countable α] {r : α → α → Prop} :
    Countable (Quot r)
    Equations
    • ⋯ = ⋯
    source
    @[instance 500]
    instance instCountableQuotient {α : Sort u} [Countable α] {s : Setoid α} :
    Countable (Quotient s)
    Equations
    • ⋯ = ⋯

    Uncountable types #

    source
    theorem uncountable_iff_not_countable (α : Sort u_1) :
    Uncountable α ↔ ¬Countable α
    source
    class Uncountable (α : Sort u_1) :
    Prop

    A type α is uncountable if it is not countable.

    • not_countable : ¬Countable α

      A type α is uncountable if it is not countable.

    Instances
      source
      theorem Uncountable.not_countable {α : Sort u_1} [self : Uncountable α] :
      ¬Countable α

      A type α is uncountable if it is not countable.

      source
      theorem not_uncountable_iff {α : Sort u} :
      ¬Uncountable α ↔ Countable α
      source
      theorem not_countable_iff {α : Sort u} :
      ¬Countable α ↔ Uncountable α
      source
      @[simp]
      theorem not_uncountable {α : Sort u} [Countable α] :
      ¬Uncountable α
      source
      @[simp]
      theorem not_countable {α : Sort u} [Uncountable α] :
      ¬Countable α
      source
      theorem Function.Injective.uncountable {α : Sort u} {β : Sort v} [Uncountable α] {f : α → β} (hf : Function.Injective f) :
      Uncountable β
      source
      theorem Function.Surjective.uncountable {α : Sort u} {β : Sort v} [Uncountable β] {f : α → β} (hf : Function.Surjective f) :
      Uncountable α
      source
      theorem not_injective_uncountable_countable {α : Sort u} {β : Sort v} [Uncountable α] [Countable β] (f : α → β) :
      ¬Function.Injective f
      source
      theorem not_surjective_countable_uncountable {α : Sort u} {β : Sort v} [Countable α] [Uncountable β] (f : α → β) :
      ¬Function.Surjective f
      source
      theorem uncountable_iff_forall_not_surjective {α : Sort u} [Nonempty α] :
      Uncountable α ↔ ∀ (f : ℕ → α), ¬Function.Surjective f
      source
      theorem Uncountable.of_equiv {β : Sort v} (α : Sort u_1) [Uncountable α] (e : α ≃ β) :
      Uncountable β
      source
      theorem Equiv.uncountable_iff {α : Sort u} {β : Sort v} (e : α ≃ β) :
      Uncountable α ↔ Uncountable β
      source
      instance instUncountableULift {β : Type v} [Uncountable β] :
      Uncountable (ULift.{u, v} β)
      Equations
      • ⋯ = ⋯
      source
      instance instUncountablePLift {α : Sort u} [Uncountable α] :
      Uncountable (PLift α)
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance instInfiniteOfUncountable {α : Sort u} [Uncountable α] :
      Infinite α
      Equations
      • ⋯ = ⋯