English
bitIndices(n) is the increasing list of indices i such that the i-th binary digit of n is 1; i.e., it collects the positions of 1s in the binary expansion of n.
Русский
bitIndices(n) — возростающий список индексов i, для которых i-я двоичная цифра числа n равна 1; т.е. собирает позиции единиц в двоичном разложении n.
LaTeX
$$bitIndices(n) = List of indices i with the i-th bit of n equal to 1$$
Lean4
theorem binaryRecFromOne_eq {zero : motive 0} {one : motive 1}
{bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (n.bit b)} (b n) (h) :
binaryRecFromOne zero one bit (Nat.bit b n) = bit b n h (binaryRecFromOne zero one bit n) := by
rw [binaryRecFromOne, binaryRec'_eq _ _ (by simp [h]), dif_neg h, binaryRecFromOne]
