English
There is a natural equivalence between natural numbers and finite sets of naturals given by bit-indices, with the forward map n ↦ n.bitIndices.toFinset and inverse map s ↦ ∑ i ∈ s, 2^i.
Русский
Существует естественная эквивалентность между натуральными числами и конечными множествами натуральных чисел через битовые индексы: n ↦ n.bitIndices.toFinset и обратное отображение s ↦ ∑ i∈s 2^i.
LaTeX
$$$equivBitIndices : \mathbb{N} \simeq \Finset(\mathbb{N})$ with
toFun(n) = n.bitIndices.toFinset, invFun(s) = \sum i\in s 2^i$$$
Lean4
/-- The equivalence between `ℕ` and `Finset ℕ` that maps `∑ i ∈ s, 2^i` to `s`. -/
@[simps]
def equivBitIndices : ℕ ≃ Finset ℕ where
toFun n := n.bitIndices.toFinset
invFun s := ∑ i ∈ s, 2 ^ i
left_inv := twoPowSum_toFinset_bitIndices
right_inv := toFinset_bitIndices_twoPowSum
