Mathlib.Logic.Denumerable

Denumerable structure

(α : Type*) extends Encodable α

Full source

/-- A denumerable type is (constructively) bijective with `ℕ`. Typeclass equivalent of `α ≃ ℕ`. -/
class Denumerable (α : Type*) extends Encodable α where
  /-- `decode` and `encode` are inverses. -/
  decode_inv : ∀ n, ∃ a ∈ decode n, encode a = n

Denumerable Type

Informal description

A denumerable type is a type `α` that is constructively bijective with the natural numbers `ℕ`. This structure extends `Encodable α` and provides the additional property that the encoding and decoding functions between `α` and `ℕ` are inverses of each other.

Denumerable.decode_isSome theorem

(α) [Denumerable α] (n : ℕ) : (decode (α := α) n).isSome

Full source

theorem decode_isSome (α) [Denumerable α] (n : ℕ) : (decode (α := α) n).isSome :=
  Option.isSome_iff_exists.2 <| (decode_inv n).imp fun _ => And.left

Decoding is Always Defined for Denumerable Types

Informal description

For any denumerable type $\alpha$ and any natural number $n$, the decoding function `decode` applied to $n$ is guaranteed to produce a valid element of $\alpha$ (i.e., `decode n` is not `none`).

Denumerable.ofNat definition

(α) [Denumerable α] (n : ℕ) : α

Full source

/-- Returns the `n`-th element of `α` indexed by the decoding. -/
def ofNat (α) [Denumerable α] (n : ℕ) : α :=
  Option.get _ (decode_isSome α n)

$n$-th element of a denumerable type

Informal description

Given a denumerable type $\alpha$ and a natural number $n$, the function returns the $n$-th element of $\alpha$ according to the decoding function. This is well-defined since the decoding function is guaranteed to produce a valid element for any $n$ (as ensured by `decode_isSome`).

Denumerable.decode_eq_ofNat theorem

(α) [Denumerable α] (n : ℕ) : decode (α := α) n = some (ofNat α n)

Full source

@[simp]
theorem decode_eq_ofNat (α) [Denumerable α] (n : ℕ) : decode (α := α) n = some (ofNat α n) :=
  Option.eq_some_of_isSome _

Decoding Yields the $n$-th Element in Denumerable Types

Informal description

For any denumerable type $\alpha$ and any natural number $n$, the decoding function applied to $n$ returns the $n$-th element of $\alpha$ (wrapped in `some`), i.e., $\mathrm{decode}_\alpha(n) = \mathrm{some}(\mathrm{ofNat}_\alpha(n))$.

Denumerable.ofNat_of_decode theorem

{n b} (h : decode (α := α) n = some b) : ofNat (α := α) n = b

Full source

@[simp]
theorem ofNat_of_decode {n b} (h : decode (α := α) n = some b) : ofNat (α := α) n = b :=
  Option.some.inj <| (decode_eq_ofNat _ _).symm.trans h

Consistency of Decoding and Enumeration in Denumerable Types

Informal description

For any denumerable type $\alpha$, if the decoding function applied to a natural number $n$ yields $\mathrm{some}(b)$ for some element $b : \alpha$, then the $n$-th element of $\alpha$ (as given by $\mathrm{ofNat}_\alpha(n)$) is equal to $b$. In other words, $\mathrm{ofNat}_\alpha(n) = b$ whenever $\mathrm{decode}_\alpha(n) = \mathrm{some}(b)$.

Denumerable.encode_ofNat theorem

(n) : encode (ofNat α n) = n

Full source

@[simp]
theorem encode_ofNat (n) : encode (ofNat α n) = n := by
  obtain ⟨a, h, e⟩ := decode_inv (α := α) n
  rwa [ofNat_of_decode h]

Encoding of $n$-th Element in Denumerable Types

Informal description

For any denumerable type $\alpha$ and any natural number $n$, the encoding function applied to the $n$-th element of $\alpha$ returns $n$, i.e., $\mathrm{encode}(\mathrm{ofNat}_\alpha(n)) = n$.

Denumerable.ofNat_encode theorem

(a) : ofNat α (encode a) = a

Full source

@[simp]
theorem ofNat_encode (a) : ofNat α (encode a) = a :=
  ofNat_of_decode (encodek _)

Encoding and Enumeration Consistency in Denumerable Types

Informal description

For any element $a$ of a denumerable type $\alpha$, the $n$-th element of $\alpha$ (where $n$ is the encoding of $a$) is equal to $a$ itself, i.e., $\mathrm{ofNat}_\alpha(\mathrm{encode}(a)) = a$.

Denumerable.eqv definition

(α) [Denumerable α] : α ≃ ℕ

Full source

/-- A denumerable type is equivalent to `ℕ`. -/
def eqv (α) [Denumerable α] : α ≃ ℕ :=
  ⟨encode, ofNat α, ofNat_encode, encode_ofNat⟩

Bijection between denumerable type and natural numbers

Informal description

For any denumerable type $\alpha$, there exists a bijection $\alpha \simeq \mathbb{N}$ consisting of the encoding function $\mathrm{encode} : \alpha \to \mathbb{N}$ and the enumeration function $\mathrm{ofNat}_\alpha : \mathbb{N} \to \alpha$, which are inverses of each other. Specifically, $\mathrm{ofNat}_\alpha \circ \mathrm{encode} = \mathrm{id}$ and $\mathrm{encode} \circ \mathrm{ofNat}_\alpha = \mathrm{id}$.

Denumerable.instInfinite instance

: Infinite α

Full source

instance (priority := 100) : Infinite α :=
  Infinite.of_surjective _ (eqv α).surjective

Denumerable Types are Infinite

Informal description

Every denumerable type $\alpha$ is infinite.

Denumerable.mk' definition

{α} (e : α ≃ ℕ) : Denumerable α

Full source

/-- A type equivalent to `ℕ` is denumerable. -/
def mk' {α} (e : α ≃ ℕ) : Denumerable α where
  encode := e
  decode := somesome ∘ e.symm
  encodek _ := congr_arg some (e.symm_apply_apply _)
  decode_inv _ := ⟨_, rfl, e.apply_symm_apply _⟩

Denumerable structure from bijection with $\mathbb{N}$

Informal description

Given a type $\alpha$ and a bijection $e : \alpha \simeq \mathbb{N}$, the function constructs a denumerable structure on $\alpha$ by defining the encoding function as $e$ and the decoding function as the composition of $e^{-1}$ with the `some` constructor.

Denumerable.ofEquiv definition

(α) {β} [Denumerable α] (e : β ≃ α) : Denumerable β

Full source

/-- Denumerability is conserved by equivalences. This is transitivity of equivalence the denumerable
way. -/
def ofEquiv (α) {β} [Denumerable α] (e : β ≃ α) : Denumerable β :=
  { Encodable.ofEquiv _ e with
    decode_inv := fun n => by
      simp [decode_ofEquiv, encode_ofEquiv] }

Denumerability via Equivalence

Informal description

Given a denumerable type $\alpha$ and a bijection $e : \beta \simeq \alpha$, the type $\beta$ is also denumerable. The encoding function for $\beta$ is defined as $\text{encode}(b) = \text{encode}(e(b))$, and the decoding function is $\text{decode}(n) = \text{decode}(n) \mathbin{\text{map}} e^{-1}$ (where $\text{map}$ is the `Option.map` operation and $e^{-1}$ is the inverse of $e$).

Denumerable.ofEquiv_ofNat theorem

(α) {β} [Denumerable α] (e : β ≃ α) (n) : @ofNat β (ofEquiv _ e) n = e.symm (ofNat α n)

Full source

@[simp]
theorem ofEquiv_ofNat (α) {β} [Denumerable α] (e : β ≃ α) (n) :
    @ofNat β (ofEquiv _ e) n = e.symm (ofNat α n) := by
  letI := ofEquiv _ e
  refine ofNat_of_decode ?_
  rw [decode_ofEquiv e]
  simp

Consistency of Enumeration under Equivalence: $\mathrm{ofNat}_\beta(n) = e^{-1}(\mathrm{ofNat}_\alpha(n))$

Informal description

For any denumerable type $\alpha$ and a bijection $e : \beta \simeq \alpha$, the $n$-th element of $\beta$ (under the denumerable structure induced by $e$) is equal to the inverse image under $e$ of the $n$-th element of $\alpha$. That is, $\mathrm{ofNat}_\beta(n) = e^{-1}(\mathrm{ofNat}_\alpha(n))$.

Denumerable.equiv₂ definition

(α β) [Denumerable α] [Denumerable β] : α ≃ β

Full source

/-- All denumerable types are equivalent. -/
def equiv₂ (α β) [Denumerable α] [Denumerable β] : α ≃ β :=
  (eqv α).trans (eqv β).symm

Bijection between any two denumerable types

Informal description

For any two denumerable types $\alpha$ and $\beta$, there exists a bijection $\alpha \simeq \beta$ obtained by composing the bijection $\alpha \simeq \mathbb{N}$ with the inverse of the bijection $\beta \simeq \mathbb{N}$.

Denumerable.nat instance

: Denumerable ℕ

Full source

instance nat : Denumerable ℕ :=
  ⟨fun _ => ⟨_, rfl, rfl⟩⟩

Natural Numbers are Denumerable

Informal description

The natural numbers $\mathbb{N}$ form a denumerable type, meaning there exists a constructive bijection between $\mathbb{N}$ and itself that preserves the encoding and decoding operations.

Denumerable.ofNat_nat theorem

(n) : ofNat ℕ n = n

Full source

@[simp]
theorem ofNat_nat (n) : ofNat ℕ n = n :=
  rfl

Identity of Natural Number Indexing in Denumerable Type

Informal description

For any natural number $n$, the $n$-th element of the denumerable type $\mathbb{N}$ is equal to $n$ itself, i.e., $\text{ofNat}(\mathbb{N}, n) = n$.

Denumerable.option instance

: Denumerable (Option α)

Full source

/-- If `α` is denumerable, then so is `Option α`. -/
instance option : Denumerable (Option α) :=
  ⟨fun n => by
    cases n with
    | zero =>
      refine ⟨none, ?_, encode_none⟩
      rw [decode_option_zero, Option.mem_def]
    | succ n =>
      refine ⟨some (ofNat α n), ?_, ?_⟩
      · rw [decode_option_succ, decode_eq_ofNat, Option.map_some', Option.mem_def]
      rw [encode_some, encode_ofNat]⟩

Denumerability of Option Types

Informal description

For any denumerable type $\alpha$, the type $\text{Option } \alpha$ is also denumerable.

Denumerable.sum instance

: Denumerable (α ⊕ β)

Full source

/-- If `α` and `β` are denumerable, then so is their sum. -/
instance sum : Denumerable (α ⊕ β) :=
  ⟨fun n => by
    suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by simpa [bit_decomp]
    simp only [decodeSum, boddDiv2_eq, decode_eq_ofNat, Option.some.injEq, Option.map_some',
      Option.mem_def, Sum.exists]
    cases bodd n <;> simp [decodeSum, bit, encodeSum, Nat.two_mul]⟩

Denumerability of Sum Types

Informal description

For any two denumerable types $\alpha$ and $\beta$, their sum type $\alpha \oplus \beta$ is also denumerable.

Denumerable.sigma instance

: Denumerable (Sigma γ)

Full source

/-- A denumerable collection of denumerable types is denumerable. -/
instance sigma : Denumerable (Sigma γ) :=
  ⟨fun n => by simp [decodeSigma]⟩

Denumerability of Dependent Pair Types

Informal description

For any family of denumerable types $\gamma$, the dependent pair type $\Sigma \gamma$ is also denumerable.

Denumerable.sigma_ofNat_val theorem

(n : ℕ) : ofNat (Sigma γ) n = ⟨ofNat α (unpair n).1, ofNat (γ _) (unpair n).2⟩

Full source

@[simp]
theorem sigma_ofNat_val (n : ℕ) :
    ofNat (Sigma γ) n = ⟨ofNat α (unpair n).1, ofNat (γ _) (unpair n).2⟩ :=
  Option.some.inj <| by rw [← decode_eq_ofNat, decode_sigma_val]; simp

$n$-th Element of Dependent Pair Type via Unpairing

Informal description

For any natural number $n$, the $n$-th element of the dependent pair type $\Sigma \gamma$ is given by $\langle a, b \rangle$, where $a$ is the $n_1$-th element of $\alpha$ and $b$ is the $n_2$-th element of $\gamma(a)$, with $(n_1, n_2) = \text{unpair}(n)$.

Denumerable.prod instance

: Denumerable (α × β)

Full source

/-- If `α` and `β` are denumerable, then so is their product. -/
instance prod : Denumerable (α × β) :=
  ofEquiv _ (Equiv.sigmaEquivProd α β).symm

Denumerability of Product Types

Informal description

For any two denumerable types $\alpha$ and $\beta$, their product $\alpha \times \beta$ is also denumerable.

Denumerable.prod_ofNat_val theorem

(n : ℕ) : ofNat (α × β) n = (ofNat α (unpair n).1, ofNat β (unpair n).2)

Full source

theorem prod_ofNat_val (n : ℕ) :
    ofNat (α × β) n = (ofNat α (unpair n).1, ofNat β (unpair n).2) := by simp

$n$-th Element of Product Type via Unpairing: $\text{ofNat}_{\alpha \times \beta}(n) = (\text{ofNat}_\alpha(n_1), \text{ofNat}_\beta(n_2))$ where $(n_1, n_2) = \text{unpair}(n)$

Informal description

For any denumerable types $\alpha$ and $\beta$, and any natural number $n$, the $n$-th element of the product type $\alpha \times \beta$ is given by $(a, b)$, where $a$ is the $n_1$-th element of $\alpha$ and $b$ is the $n_2$-th element of $\beta$, with $(n_1, n_2) = \text{unpair}(n)$.

Denumerable.prod_nat_ofNat theorem

: ofNat (ℕ × ℕ) = unpair

Full source

@[simp]
theorem prod_nat_ofNat : ofNat (ℕℕ × ℕ) = unpair := by funext; simp

Enumeration of $\mathbb{N} \times \mathbb{N}$ via Unpairing

Informal description

The enumeration function for the product type $\mathbb{N} \times \mathbb{N}$ coincides with the unpairing function, i.e., $\mathrm{ofNat}_{\mathbb{N} \times \mathbb{N}} = \mathrm{unpair}$.

Denumerable.int instance

: Denumerable ℤ

Full source

instance int : Denumerable ℤ :=
  Denumerable.mk' Equiv.intEquivNat

Denumerability of Integers

Informal description

The integers $\mathbb{Z}$ form a denumerable type, meaning there exists a constructive bijection between $\mathbb{Z}$ and $\mathbb{N}$.

Denumerable.pnat instance

: Denumerable ℕ+

Full source

instance pnat : Denumerable ℕ+ :=
  Denumerable.mk' Equiv.pnatEquivNat

Denumerability of Positive Natural Numbers

Informal description

The type of positive natural numbers $\mathbb{N}^+$ is denumerable, meaning there exists a constructive bijection between $\mathbb{N}^+$ and $\mathbb{N}$.

Denumerable.ulift instance

: Denumerable (ULift α)

Full source

/-- The lift of a denumerable type is denumerable. -/
instance ulift : Denumerable (ULift α) :=
  ofEquiv _ Equiv.ulift

Denumerability of Lifted Types

Informal description

For any denumerable type $\alpha$, the lifted type $\text{ULift}\,\alpha$ is also denumerable.

Denumerable.plift instance

: Denumerable (PLift α)

Full source

/-- The lift of a denumerable type is denumerable. -/
instance plift : Denumerable (PLift α) :=
  ofEquiv _ Equiv.plift

Denumerability of Lifted Types

Informal description

For any denumerable type $\alpha$, the lifted type $\text{PLift}\,\alpha$ is also denumerable.

Denumerable.pair definition

: α × α ≃ α

Full source

/-- If `α` is denumerable, then `α × α` and `α` are equivalent. -/
def pair : α × αα × α ≃ α :=
  equiv₂ _ _

Bijection between a denumerable type and its square

Informal description

For any denumerable type $\alpha$, there exists a bijection between $\alpha \times \alpha$ and $\alpha$.

Nat.Subtype.exists_succ theorem

(x : s) : ∃ n, (x : ℕ) + n + 1 ∈ s

Full source

theorem exists_succ (x : s) : ∃ n, (x : ℕ) + n + 1 ∈ s := by
  by_contra h
  have (a : ℕ) (ha : a ∈ s) : a < x + 1 :=
    lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]⟩
  classical
  exact Fintype.false
    ⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap
      (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy) (by simp [-Multiset.range_succ])).toFinset,
      by simpa [Subtype.ext_iff_val, Multiset.mem_filter, -Multiset.range_succ] ⟩

Existence of Successor in Natural Number Subsets

Informal description

For any element $x$ in a subset $s$ of natural numbers, there exists a natural number $n$ such that $x + n + 1$ is also in $s$.

Nat.Subtype.succ definition

(x : s) : s

Full source

/-- Returns the next natural in a set, according to the usual ordering of `ℕ`. -/
def succ (x : s) : s :=
  have h : ∃ m, (x : ℕ) + m + 1 ∈ s := exists_succ x
  ⟨↑x + Nat.find h + 1, Nat.find_spec h⟩

Successor function for natural number subsets

Informal description

Given a subset $ s $ of natural numbers and an element $ x \in s $, the function returns the next element in $ s $ according to the usual ordering of $ \mathbb{N} $. Specifically, it finds the smallest natural number $ m $ such that $ x + m + 1 \in s $ and returns $ x + m + 1 $.

Nat.Subtype.succ_le_of_lt theorem

{x y : s} (h : y < x) : succ y ≤ x

Full source

theorem succ_le_of_lt {x y : s} (h : y < x) : succ y ≤ x :=
  have hx : ∃ m, (y : ℕ) + m + 1 ∈ s := exists_succ _
  let ⟨k, hk⟩ := Nat.exists_eq_add_of_lt h
  have : Nat.find hx ≤ k := Nat.find_min' _ (hk ▸ x.2)
  show (y : ℕ) + Nat.find hx + 1 ≤ x by omega

Successor Bound in Infinite Subset of Natural Numbers

Informal description

For any elements $x$ and $y$ in an infinite subset $s$ of natural numbers, if $y < x$, then the successor of $y$ in $s$ is less than or equal to $x$.

Nat.Subtype.le_succ_of_forall_lt_le theorem

{x y : s} (h : ∀ z < x, z ≤ y) : x ≤ succ y

Full source

theorem le_succ_of_forall_lt_le {x y : s} (h : ∀ z < x, z ≤ y) : x ≤ succ y :=
  have hx : ∃ m, (y : ℕ) + m + 1 ∈ s := exists_succ _
  show (x : ℕ) ≤ (y : ℕ) + Nat.find hx + 1 from
    le_of_not_gt fun hxy =>
      (h ⟨_, Nat.find_spec hx⟩ hxy).not_lt <|
        (by omega : (y : ℕ) < (y : ℕ) + Nat.find hx + 1)

Order Relation Between Elements and Successor in Infinite Subset of Natural Numbers

Informal description

For any elements $x$ and $y$ in an infinite subset $s$ of natural numbers, if every element $z \in s$ with $z < x$ satisfies $z \leq y$, then $x$ is less than or equal to the successor of $y$ in $s$, i.e., $x \leq \text{succ}(y)$.

Nat.Subtype.lt_succ_self theorem

(x : s) : x < succ x

Full source

theorem lt_succ_self (x : s) : x < succ x :=
  calc
    (x : ℕ) ≤ (x + _)  := le_add_right ..
    _       < (succ x) := Nat.lt_succ_self (x + _)

Element is Less Than its Successor in Infinite Subset of Natural Numbers

Informal description

For any element $x$ in an infinite subset $s$ of natural numbers, $x$ is strictly less than its successor in $s$, i.e., $x < \text{succ}(x)$.

Nat.Subtype.lt_succ_iff_le theorem

{x y : s} : x < succ y ↔ x ≤ y

Full source

theorem lt_succ_iff_le {x y : s} : x < succ y ↔ x ≤ y :=
  ⟨fun h => le_of_not_gt fun h' => not_le_of_gt h (succ_le_of_lt h'), fun h =>
    lt_of_le_of_lt h (lt_succ_self _)⟩

Order Relation Between Elements and Successor in Infinite Subset of Natural Numbers

Informal description

For any elements $x$ and $y$ in an infinite subset $s$ of natural numbers, $x$ is strictly less than the successor of $y$ in $s$ if and only if $x$ is less than or equal to $y$, i.e., $x < \text{succ}(y) \leftrightarrow x \leq y$.

Nat.Subtype.ofNat definition

(s : Set ℕ) [DecidablePred (· ∈ s)] [Infinite s] : ℕ → s

Full source

/-- Returns the `n`-th element of a set, according to the usual ordering of `ℕ`. -/
def ofNat (s : Set ℕ) [DecidablePred (· ∈ s)] [Infinite s] : ℕ → s
  | 0 => ⊥
  | n + 1 => succ (ofNat s n)

$n$-th element of an infinite subset of natural numbers

Informal description

Given an infinite subset $s$ of natural numbers with decidable membership, the function returns the $n$-th element of $s$ according to the usual ordering of $\mathbb{N}$. Specifically, it is defined recursively as: - For $n = 0$, it returns the least element of $s$. - For $n = k + 1$, it returns the successor (in $s$) of the $k$-th element.

Nat.Subtype.ofNat_surjective theorem

: Surjective (ofNat s)

Full source

theorem ofNat_surjective : Surjective (ofNat s)
  | ⟨x, hx⟩ => by
    set t : List s :=
      ((List.range x).filter fun y => y ∈ s).pmap
        (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
        (by intros a ha; simpa using (List.mem_filter.mp ha).2) with ht
    have hmt : ∀ {y : s}, y ∈ ty ∈ t ↔ y < ⟨x, hx⟩ := by
      simp [List.mem_filter, Subtype.ext_iff_val, ht]
    cases hmax : List.maximum t with
    | bot =>
      refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (a := (⊥ : s)) ?_)⟩
      rwa [← List.maximum_eq_bot.1 hmax, hmt]
    | coe m =>
      have wf : ↑m < x := by simpa using hmt.mp (List.maximum_mem hmax)
      rcases ofNat_surjective m with ⟨a, rfl⟩
      refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩
      exact le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax
  termination_by n => n.val

Surjectivity of the Enumeration Function for Infinite Subsets of Natural Numbers

Informal description

For any infinite subset $s$ of natural numbers with decidable membership, the function that maps each natural number $n$ to the $n$-th element of $s$ is surjective. That is, every element of $s$ is the image of some natural number under this function.

Nat.Subtype.ofNat_range theorem

: Set.range (ofNat s) = Set.univ

Full source

@[simp]
theorem ofNat_range : Set.range (ofNat s) = Set.univ :=
  ofNat_surjective.range_eq

Range of Enumeration Function for Infinite Subset of Natural Numbers is Universal Set

Informal description

For any infinite subset $s$ of natural numbers with decidable membership, the range of the enumeration function that maps each natural number $n$ to the $n$-th element of $s$ is equal to the universal set of $s$. That is, $\text{range}(\text{ofNat}_s) = \text{univ}$.

Nat.Subtype.coe_comp_ofNat_range theorem

: Set.range ((↑) ∘ ofNat s : ℕ → ℕ) = s

Full source

@[simp]
theorem coe_comp_ofNat_range : Set.range ((↑) ∘ ofNat s : ℕ → ℕ) = s := by
  rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]

Range of Inclusion-Composed Enumeration Function Equals Subset

Informal description

For any infinite subset $s$ of natural numbers with decidable membership, the range of the composition of the enumeration function $\text{ofNat}_s$ (which maps each natural number $n$ to the $n$-th element of $s$) with the natural inclusion map $\uparrow$ (from $s$ to $\mathbb{N}$) is equal to $s$ itself. That is, $\text{range}(\uparrow \circ \text{ofNat}_s) = s$.

Nat.Subtype.denumerable definition

(s : Set ℕ) [DecidablePred (· ∈ s)] [Infinite s] : Denumerable s

Full source

/-- Any infinite set of naturals is denumerable. -/
def denumerable (s : Set ℕ) [DecidablePred (· ∈ s)] [Infinite s] : Denumerable s :=
  Denumerable.ofEquiv ℕ
    { toFun := toFunAux
      invFun := ofNat s
      left_inv := leftInverse_of_surjective_of_rightInverse ofNat_surjective right_inverse_aux
      right_inv := right_inverse_aux }

Denumerability of infinite subsets of natural numbers

Informal description

For any infinite subset $s$ of natural numbers with decidable membership, the type $s$ is denumerable. This is established by constructing a bijection between $s$ and $\mathbb{N}$ using the $n$-th element function and its inverse.

Denumerable.ofEncodableOfInfinite definition

(α : Type*) [Encodable α] [Infinite α] : Denumerable α

Full source

/-- An infinite encodable type is denumerable. -/
def ofEncodableOfInfinite (α : Type*) [Encodable α] [Infinite α] : Denumerable α := by
  letI := @decidableRangeEncode α _
  letI : Infinite (Set.range (@encode α _)) :=
    Infinite.of_injective _ (Equiv.ofInjective _ encode_injective).injective
  letI := Nat.Subtype.denumerable (Set.range (@encode α _))
  exact Denumerable.ofEquiv (Set.range (@encode α _)) (equivRangeEncode α)

Denumerability of infinite encodable types

Informal description

Given an infinite encodable type $\alpha$, the type $\alpha$ is denumerable. This is established by constructing a bijection between $\alpha$ and $\mathbb{N}$ via the encoding function $\text{encode} : \alpha \to \mathbb{N}$ and its partial inverse $\text{decode} : \mathbb{N} \to \text{Option } \alpha$, ensuring that they are inverses of each other. The proof leverages the denumerability of infinite subsets of $\mathbb{N}$ and the equivalence between $\alpha$ and the range of its encoding function.

nonempty_denumerable theorem

(α : Type*) [Countable α] [Infinite α] : Nonempty (Denumerable α)

Full source

/-- See also `nonempty_encodable`, `nonempty_fintype`. -/
theorem nonempty_denumerable (α : Type*) [Countable α] [Infinite α] : Nonempty (Denumerable α) :=
  (nonempty_encodable α).map fun h => @Denumerable.ofEncodableOfInfinite _ h _

Existence of Denumerable Structure for Countable Infinite Types

Informal description

For any countable and infinite type $\alpha$, there exists a denumerable structure on $\alpha$.

nonempty_denumerable_iff theorem

{α : Type*} : Nonempty (Denumerable α) ↔ Countable α ∧ Infinite α

Full source

theorem nonempty_denumerable_iff {α : Type*} :
    NonemptyNonempty (Denumerable α) ↔ Countable α ∧ Infinite α :=
  ⟨fun ⟨_⟩ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ nonempty_denumerable _⟩

Denumerability Criterion: $\alpha$ is denumerable if and only if it is countable and infinite

Informal description

For any type $\alpha$, there exists a denumerable structure on $\alpha$ if and only if $\alpha$ is both countable and infinite.

nonempty_equiv_of_countable instance

[Countable α] [Infinite α] [Countable β] [Infinite β] : Nonempty (α ≃ β)

Full source

instance nonempty_equiv_of_countable [Countable α] [Infinite α] [Countable β] [Infinite β] :
    Nonempty (α ≃ β) := by
  cases nonempty_denumerable α
  cases nonempty_denumerable β
  exact ⟨(Denumerable.eqv _).trans (Denumerable.eqv _).symm⟩

Bijection between Countable Infinite Types

Informal description

For any two countable and infinite types $\alpha$ and $\beta$, there exists a bijection between them, i.e., $\alpha \simeq \beta$.

Implementation notes