English
For any infinite subset s of ℕ, there exists a strictly increasing enumeration of s, i.e., an order-embedding of ℕ into s whose range is s.
Русский
Для любого бесконечного подмножества s натуральных чисел существует упорядоченная(increasing) нумерация элементов s — вложение ℕ в s, чьё множество образов равно s.
LaTeX
$$$$[\DecidablePred(\cdot \in s)]\ :\ Set.range(\mathrm{Nat.orderEmbeddingOfSet}(s)) = s.$$$$
Lean4
/-- An order embedding from `ℕ` to itself with a specified range -/
def orderEmbeddingOfSet [DecidablePred (· ∈ s)] : ℕ ↪o ℕ :=
(RelEmbedding.orderEmbeddingOfLTEmbedding
(RelEmbedding.natLT (Nat.Subtype.ofNat s) fun _ => Nat.Subtype.lt_succ_self _)).trans
(OrderEmbedding.subtype s)
