bitIndices_sorted — Mathlib

English

For all n, bitIndices(n) is strictly increasing under the usual order on natural numbers.

Русский

Для любого n список bitIndices(n) упорядочен по естественному порядку натуральных чисел (возрастание).

LaTeX

$$$\text{List}.Sorted(\"<\",)\; n.bitIndices$$$

Lean4

@[simp]
theorem bitIndices_sorted {n : ℕ} : n.bitIndices.Sorted (· < ·) := by
  induction n using binaryRec with
  | zero => simp
  | bit b n
    hs =>
    suffices List.Pairwise (fun a b ↦ a < b) n.bitIndices by
      cases b <;> simpa [List.Sorted, bit_false, bit_true, List.pairwise_map]
    exact List.Pairwise.imp (by simp) hs

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