English
There exists an order-preserving bijection between the natural numbers and the family of finite subsets of the natural numbers when those subsets are endowed with the colexicographic order. Concretely, the map n ↦ toColex(equivBitIndices(n)) gives an order isomorphism ℕ ≃o Colex(Finset(ℕ)) with inverse s ↦ equivBitIndices.symm(ofColex s).
Русский
Существует биективное отображение, сохраняющее порядок, между множеством естественных чисел и семейством конечных подмножеств ℕ, если подмножества упорядочены по коэкседическому порядку. Конкретно, n ↦ toColex(equivBitIndices(n)) образует порядковое изоморфизм ℕ ≃o Colex(Finset(ℕ)) с обратным отображением equivBitIndices.symm(ofColex s).
LaTeX
$$$\\exists \\phi:\\mathbb{N} \\simeq_o \\operatorname{Colex}(\\operatorname{Finset}(\\mathbb{N}))\\;\\text{such that}\\; \\phi(n)=\\operatorname{toColex}(\\operatorname{equivBitIndices}(n))\\;\\text{and}\\; \\phi^{-1}(S)=\\operatorname{equivBitIndices}(\\operatorname{ofColex}(S)).$$$
Lean4
/-- The equivalence `Nat.equivBitIndices` enumerates `Finset ℕ` in colexicographic order. -/
@[simps]
def orderIsoColex : ℕ ≃o Colex (Finset ℕ)
where
toFun n := toColex (equivBitIndices n)
invFun s := equivBitIndices.symm (ofColex s)
left_inv n := equivBitIndices.symm_apply_apply n
right_inv s := equivBitIndices.apply_symm_apply _
map_rel_iff' := by simp [← (Finset.geomSum_le_geomSum_iff_toColex_le_toColex rfl.le)]
