toFinset_bitIndices_twoPowSum — Mathlib

English

The bit-indices of a natural sum equals the original finite set: (∑ i ∈ s, 2^i).bitIndices.toFinset = s.

Русский

Битовые индексы суммы дают исходное множество: (∑ i∈s 2^i).bitIndices.toFinset = s.

LaTeX

$$$ (\sum i \in s, 2^i).\text{bitIndices}.toFinset = s $$$

Lean4

@[simp]
theorem toFinset_bitIndices_twoPowSum (s : Finset ℕ) : (∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s := by
  simp [← (geomSum_injective rfl.le).eq_iff, List.sum_toFinset _ Nat.bitIndices_sorted.nodup]

Похожие утверждения