twoPowSum_toFinset_bitIndices

Mathlib.Combinatorics.Colex

URI: https://scilib.ai/kg/mathlib#Finset.twoPowSum_toFinset_bitIndices

← MathLib Explorer

English

For any n, the sum of 2^i over i in s equals the natural number whose bit-indices are s.

Русский

Сумма 2^i по i∈s равна числу, чьи битовые индексы — это s.

LaTeX

$$$\sum_{i\in s} 2^i = n \iff \text{bits}(n)=s$ (in appropriate encoding)$$

Lean4

@[simp]
theorem twoPowSum_toFinset_bitIndices (n : ℕ) : ∑ i ∈ n.bitIndices.toFinset, 2 ^ i = n := by
  simp [List.sum_toFinset _ Nat.bitIndices_sorted.nodup]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru