Enumeration in increasing rank

Abstract

An injective natural ranking of an infinite set determines a literal enumeration.

Theorem 1.1 (An enumeration increasing in an injective rank).

$$\forall S\in \mathrm{Set}\left(\mathbb{N}\right),\forall rank\in \mathbb{N}\to \mathbb{N},\left(\mathrm{Infinite}\left(S\right)\wedge \mathrm{InjOn}\left(rank,S\right)\right)\Rightarrow \left(\exists pi\in \mathbb{N}\to \mathbb{N},\left(\mathrm{Injective}\left(pi\right)\wedge \mathrm{range}\left(pi\right)=S\right)\wedge \left(\forall i\in \mathbb{N},\forall j\in \mathbb{N},i<j\Rightarrow \mathrm{rank}\left(\mathrm{pi}\left(i\right)\right)<\mathrm{rank}\left(\mathrm{pi}\left(j\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Permutation/LeSaulnierVijayLowerDensityRefutationEnumeration.enumerateRank (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every infinite subset S of the natural numbers and every natural-valued function rank injective on S, there is an injective map pi from the natural numbers onto S with rank(pi(i)) strictly increasing in i. Enumerate the infinite image rank(S) by Mathlib’s Nat.nth, then select its unique preimages in S. Infinite(S) and InjOn(rank,S) denote these two hypotheses; Injective(pi) and range(pi)=S state the literal permutation conclusion.

References

• Truth anchor: D5/S3/Combinatorics/Permutation/LeSaulnierVijayLowerDensityRefutationEnumeration.enumerateRank