two_pow_le_of_mem_bitIndices — Mathlib

English

Let L be a finite list of natural numbers that is strictly increasing. Then the sum of 2^i over i in L has bitIndices equal to L.

Русский

Пусть L — конечный список натуральных чисел, упорядоченный по возрастанию. Тогда сумма 2^i по i из L имеет битовые индексы, равные L.

LaTeX

$$$\forall L \in \mathrm{List}(\mathbb{N}), \ \mathrm{List.Sorted}(L, <) \Rightarrow \bigg( \big( \sum_{i \in L} 2^{i} \big).\mathrm{bitIndices} = L \bigg)$$$

Lean4

theorem two_pow_le_of_mem_bitIndices (ha : a ∈ n.bitIndices) : 2 ^ a ≤ n :=
  by
  rw [← twoPowSum_bitIndices n]
  exact List.single_le_sum (by simp) _ <| mem_map_of_mem ha

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