Mathlib.Data.Countable.Defs

Countable structure

(α : Sort u)

Full source

/-- A type `α` is countable if there exists an injective map `α → ℕ`. -/
@[mk_iff countable_iff_exists_injective]
class Countable (α : Sort u) : Prop where
  /-- A type `α` is countable if there exists an injective map `α → ℕ`. -/
  exists_injective_nat' : ∃ f : α → ℕ, Injective f

Countable type

Informal description

A type $\alpha$ is called *countable* if there exists an injective function from $\alpha$ to the natural numbers $\mathbb{N}$.

Countable.exists_injective_nat theorem

(α : Sort u) [Countable α] : ∃ f : α → ℕ, Injective f

Full source

lemma Countable.exists_injective_nat (α : Sort u) [Countable α] : ∃ f : α → ℕ, Injective f :=
  Countable.exists_injective_nat'

Existence of Injection from Countable Type to Natural Numbers

Informal description

For any countable type $\alpha$, there exists an injective function $f: \alpha \to \mathbb{N}$.

instCountableNat instance

: Countable ℕ

Full source

instance : Countable ℕ :=
  ⟨⟨id, injective_id⟩⟩

Countability of Natural Numbers

Informal description

The type of natural numbers $\mathbb{N}$ is countable.

Function.Injective.countable theorem

[Countable β] {f : α → β} (hf : Injective f) : Countable α

Full source

protected theorem Function.Injective.countable [Countable β] {f : α → β} (hf : Injective f) :
    Countable α :=
  let ⟨g, hg⟩ := exists_injective_nat β
  ⟨⟨g ∘ f, hg.comp hf⟩⟩

Injectivity Preserves Countability

Informal description

Let $\alpha$ and $\beta$ be types where $\beta$ is countable. If there exists an injective function $f: \alpha \to \beta$, then $\alpha$ is also countable.

Function.Surjective.countable theorem

[Countable α] {f : α → β} (hf : Surjective f) : Countable β

Full source

protected theorem Function.Surjective.countable [Countable α] {f : α → β} (hf : Surjective f) :
    Countable β :=
  (injective_surjInv hf).countable

Surjectivity Preserves Countability

Informal description

Let $\alpha$ and $\beta$ be types where $\alpha$ is countable. If there exists a surjective function $f: \alpha \to \beta$, then $\beta$ is also countable.

exists_surjective_nat theorem

(α : Sort u) [Nonempty α] [Countable α] : ∃ f : ℕ → α, Surjective f

Full source

theorem exists_surjective_nat (α : Sort u) [Nonempty α] [Countable α] : ∃ f : ℕ → α, Surjective f :=
  let ⟨f, hf⟩ := exists_injective_nat α
  ⟨invFun f, invFun_surjective hf⟩

Existence of Surjection from Natural Numbers to Countable Type

Informal description

For any nonempty and countable type $\alpha$, there exists a surjective function $f: \mathbb{N} \to \alpha$.

countable_iff_exists_surjective theorem

[Nonempty α] : Countable α ↔ ∃ f : ℕ → α, Surjective f

Full source

theorem countable_iff_exists_surjective [Nonempty α] : CountableCountable α ↔ ∃ f : ℕ → α, Surjective f :=
  ⟨@exists_surjective_nat _ _, fun ⟨_, hf⟩ ↦ hf.countable⟩

Countability Criterion via Surjection from Natural Numbers

Informal description

For any nonempty type $\alpha$, $\alpha$ is countable if and only if there exists a surjective function $f: \mathbb{N} \to \alpha$.

Countable.of_equiv theorem

(α : Sort*) [Countable α] (e : α ≃ β) : Countable β

Full source

theorem Countable.of_equiv (α : Sort*) [Countable α] (e : α ≃ β) : Countable β :=
  e.symm.injective.countable

Countability is Preserved under Type Equivalence

Informal description

Let $\alpha$ and $\beta$ be types with $\alpha$ countable, and let $e : \alpha \simeq \beta$ be a bijection between them. Then $\beta$ is also countable.

Equiv.countable_iff theorem

(e : α ≃ β) : Countable α ↔ Countable β

Full source

theorem Equiv.countable_iff (e : α ≃ β) : CountableCountable α ↔ Countable β :=
  ⟨fun h => @Countable.of_equiv _ _ h e, fun h => @Countable.of_equiv _ _ h e.symm⟩

Countability is Preserved under Bijection: $\text{Countable}(\alpha) \leftrightarrow \text{Countable}(\beta)$

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the type $\alpha$ is countable if and only if $\beta$ is countable.

instCountableULift instance

{β : Type v} [Countable β] : Countable (ULift.{u} β)

Full source

instance {β : Type v} [Countable β] : Countable (ULift.{u} β) :=
  Countable.of_equiv _ Equiv.ulift.symm

Countability of Universe-Lifted Types

Informal description

For any countable type $\beta$ in universe `v`, the universe-lifted type $\text{ULift}\ \beta$ in any universe `u` is also countable.

instCountablePLift instance

[Countable α] : Countable (PLift α)

Full source

instance [Countable α] : Countable (PLift α) :=
  Equiv.plift.injective.countable

Countability of Universe-Lifted Types

Informal description

For any countable type $\alpha$, the type `PLift α` (which represents $\alpha$ lifted to a higher universe) is also countable.

Subsingleton.to_countable instance

[Subsingleton α] : Countable α

Full source

instance (priority := 100) Subsingleton.to_countable [Subsingleton α] : Countable α :=
  ⟨⟨fun _ => 0, fun x y _ => Subsingleton.elim x y⟩⟩

Subsingleton Types are Countable

Informal description

Every subsingleton type $\alpha$ (a type with at most one element) is countable.

Subtype.countable instance

[Countable α] {p : α → Prop} : Countable { x // p x }

Full source

instance (priority := 500) Subtype.countable [Countable α] {p : α → Prop} :
    Countable { x // p x } :=
  Subtype.val_injective.countable

Countability of Subtypes of Countable Types

Informal description

For any countable type $\alpha$ and predicate $p$ on $\alpha$, the subtype $\{x \mid p(x)\}$ is also countable.

instCountableFin instance

{n : ℕ} : Countable (Fin n)

Full source

instance {n : ℕ} : Countable (Fin n) :=
  Function.Injective.countable (@Fin.eq_of_val_eq n)

Countability of Finite Ordinals

Informal description

For any natural number $n$, the type $\text{Fin}(n)$ of finite ordinals is countable.

Finite.to_countable instance

[Finite α] : Countable α

Full source

instance (priority := 100) Finite.to_countable [Finite α] : Countable α :=
  let ⟨_, ⟨e⟩⟩ := Finite.exists_equiv_fin α
  Countable.of_equiv _ e.symm

Countability of Finite Types

Informal description

Every finite type $\alpha$ is countable.

instCountablePUnit instance

: Countable PUnit.{u}

Full source

instance : Countable PUnitPUnit.{u} :=
  Subsingleton.to_countable

Countability of the Unit Type

Informal description

The type `PUnit` (the unit type with a single element) is countable.

Prop.countable instance

(p : Prop) : Countable p

Full source

instance (priority := 100) Prop.countable (p : Prop) : Countable p :=
  Subsingleton.to_countable

Countability of Proposition Types

Informal description

For any proposition $p$, the type associated with $p$ is countable.

Bool.countable instance

: Countable Bool

Full source

instance Bool.countable : Countable Bool :=
  ⟨⟨fun b => cond b 0 1, Bool.injective_iff.2 Nat.one_ne_zero⟩⟩

Countability of Boolean Type

Informal description

The type of booleans is countable.

Prop.countable' instance

: Countable Prop

Full source

instance Prop.countable' : Countable Prop :=
  Countable.of_equiv Bool Equiv.propEquivBool.symm

Countability of the Type of Propositions

Informal description

The type of propositions `Prop` is countable.

Quotient.countable instance

[Countable α] {r : α → α → Prop} : Countable (Quot r)

Full source

instance (priority := 500) Quotient.countable [Countable α] {r : α → α → Prop} :
    Countable (Quot r) :=
  Quot.mk_surjective.countable

Countability of Quotient Types

Informal description

For any countable type $\alpha$ and equivalence relation $r$ on $\alpha$, the quotient type $\alpha / r$ is also countable.

instCountableQuotient instance

[Countable α] {s : Setoid α} : Countable (Quotient s)

Full source

instance (priority := 500) [Countable α] {s : Setoid α} : Countable (Quotient s) :=
  (inferInstance : Countable (@Quot α _))

Countability of Quotient Types by Setoids

Informal description

For any countable type $\alpha$ and setoid $s$ on $\alpha$, the quotient type $\alpha / s$ is also countable.

Uncountable structure

(α : Sort*)

Full source

/-- A type `α` is uncountable if it is not countable. -/
@[mk_iff uncountable_iff_not_countable]
class Uncountable (α : Sort*) : Prop where
  /-- A type `α` is uncountable if it is not countable. -/
  not_countable : ¬Countable α

Uncountable type

Informal description

A type $\alpha$ is called *uncountable* if it is not countable, meaning there does not exist a bijection between $\alpha$ and the natural numbers.

not_uncountable_iff theorem

: ¬Uncountable α ↔ Countable α

Full source

lemma not_uncountable_iff : ¬Uncountable α¬Uncountable α ↔ Countable α := by
  rw [uncountable_iff_not_countable, not_not]

Equivalence of Countable and Not Uncountable Types

Informal description

A type $\alpha$ is not uncountable if and only if it is countable, i.e., $\neg \text{Uncountable}(\alpha) \leftrightarrow \text{Countable}(\alpha)$.

not_countable_iff theorem

: ¬Countable α ↔ Uncountable α

Full source

lemma not_countable_iff : ¬Countable α¬Countable α ↔ Uncountable α := (uncountable_iff_not_countable α).symm

Equivalence of Non-Countability and Uncountability

Informal description

A type $\alpha$ is not countable if and only if it is uncountable, i.e., $\neg \text{Countable}(\alpha) \leftrightarrow \text{Uncountable}(\alpha)$.

not_uncountable theorem

[Countable α] : ¬Uncountable α

Full source

@[simp]
lemma not_uncountable [Countable α] : ¬Uncountable α := not_uncountable_iff.2 ‹_›

Countable implies not uncountable

Informal description

If a type $\alpha$ is countable, then it is not uncountable.

not_countable theorem

[Uncountable α] : ¬Countable α

Full source

@[simp]
lemma not_countable [Uncountable α] : ¬Countable α := Uncountable.not_countable

Uncountable implies not countable

Informal description

If a type $\alpha$ is uncountable, then it is not countable.

Function.Injective.uncountable theorem

[Uncountable α] {f : α → β} (hf : Injective f) : Uncountable β

Full source

protected theorem Function.Injective.uncountable [Uncountable α] {f : α → β} (hf : Injective f) :
    Uncountable β :=
  ⟨fun _ ↦ not_countable hf.countable⟩

Injectivity Preserves Uncountability

Informal description

Let $\alpha$ be an uncountable type and $f : \alpha \to \beta$ be an injective function. Then $\beta$ is also uncountable.

Function.Surjective.uncountable theorem

[Uncountable β] {f : α → β} (hf : Surjective f) : Uncountable α

Full source

protected theorem Function.Surjective.uncountable [Uncountable β] {f : α → β} (hf : Surjective f) :
    Uncountable α := (injective_surjInv hf).uncountable

Surjectivity Preserves Uncountability

Informal description

Let $\beta$ be an uncountable type and $f : \alpha \to \beta$ be a surjective function. Then $\alpha$ is also uncountable.

not_injective_uncountable_countable theorem

[Uncountable α] [Countable β] (f : α → β) : ¬Injective f

Full source

lemma not_injective_uncountable_countable [Uncountable α] [Countable β] (f : α → β) :
    ¬Injective f := fun hf ↦ not_countable hf.countable

No Injection from Uncountable to Countable Types

Informal description

If $\alpha$ is an uncountable type and $\beta$ is a countable type, then there does not exist an injective function $f: \alpha \to \beta$.

not_surjective_countable_uncountable theorem

[Countable α] [Uncountable β] (f : α → β) : ¬Surjective f

Full source

lemma not_surjective_countable_uncountable [Countable α] [Uncountable β] (f : α → β) :
    ¬Surjective f := fun hf ↦
  not_countable hf.countable

No Surjection from Countable to Uncountable Types

Informal description

If $\alpha$ is a countable type and $\beta$ is an uncountable type, then there does not exist a surjective function $f: \alpha \to \beta$.

uncountable_iff_forall_not_surjective theorem

[Nonempty α] : Uncountable α ↔ ∀ f : ℕ → α, ¬Surjective f

Full source

theorem uncountable_iff_forall_not_surjective [Nonempty α] :
    UncountableUncountable α ↔ ∀ f : ℕ → α, ¬Surjective f := by
  rw [← not_countable_iff, countable_iff_exists_surjective, not_exists]

Characterization of Uncountable Types via Surjections from $\mathbb{N}$

Informal description

For any nonempty type $\alpha$, $\alpha$ is uncountable if and only if for every function $f \colon \mathbb{N} \to \alpha$, $f$ is not surjective.

Uncountable.of_equiv theorem

(α : Sort*) [Uncountable α] (e : α ≃ β) : Uncountable β

Full source

theorem Uncountable.of_equiv (α : Sort*) [Uncountable α] (e : α ≃ β) : Uncountable β :=
  e.injective.uncountable

Uncountability is Preserved by Bijection

Informal description

If a type $\alpha$ is uncountable and there exists a bijection $e : \alpha \simeq \beta$ between $\alpha$ and another type $\beta$, then $\beta$ is also uncountable.

Equiv.uncountable_iff theorem

(e : α ≃ β) : Uncountable α ↔ Uncountable β

Full source

theorem Equiv.uncountable_iff (e : α ≃ β) : UncountableUncountable α ↔ Uncountable β :=
  ⟨fun h => @Uncountable.of_equiv _ _ h e, fun h => @Uncountable.of_equiv _ _ h e.symm⟩

Uncountability is Preserved Under Bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the type $\alpha$ is uncountable if and only if $\beta$ is uncountable.

instUncountableULift instance

{β : Type v} [Uncountable β] : Uncountable (ULift.{u} β)

Full source

instance {β : Type v} [Uncountable β] : Uncountable (ULift.{u} β) :=
  .of_equiv _ Equiv.ulift.symm

Uncountability of Lifted Types

Informal description

For any uncountable type $\beta$, the lifted type $\text{ULift} \beta$ is also uncountable.

instUncountablePLift instance

[Uncountable α] : Uncountable (PLift α)

Full source

instance [Uncountable α] : Uncountable (PLift α) :=
  .of_equiv _ Equiv.plift.symm

Uncountability of Lifted Types

Informal description

For any uncountable type $\alpha$, the lifted type $\mathrm{PLift}\,\alpha$ is also uncountable.

instInfiniteOfUncountable instance

[Uncountable α] : Infinite α

Full source

instance (priority := 100) [Uncountable α] : Infinite α :=
  ⟨fun _ ↦ not_countable (α := α) inferInstance⟩

Uncountable Types are Infinite

Informal description

Every uncountable type $\alpha$ is infinite.