exists_most_significant_bit — Mathlib

English

For every nonzero n, there exists an index i such that testBit n i is true and for all j > i, testBit n j is false.

Русский

Для любого n ≠ 0 существует i, такое что testBit(n,i)=true и для всех j > i testBit(n,j)=false.

LaTeX

$$$ n\neq 0 \Rightarrow \exists i\, (testBit(n,i)=true) \land \forall j, i

Lean4

theorem exists_most_significant_bit {n : ℕ} (h : n ≠ 0) : ∃ i, testBit n i = true ∧ ∀ j, i < j → testBit n j = false :=
  by
  induction n using Nat.binaryRec with
  | zero => exact False.elim (h rfl)
  | bit b n hn => ?_
  by_cases h' : n = 0
  · subst h'
    rw [show b = true by
        revert h
        cases b <;> simp]
    refine ⟨0, ⟨by rw [testBit_bit_zero], fun j hj => ?_⟩⟩
    obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (ne_of_gt hj)
    rw [testBit_bit_succ, zero_testBit]
  · obtain ⟨k, ⟨hk, hk'⟩⟩ := hn h'
    refine ⟨k + 1, ⟨by rw [testBit_bit_succ, hk], fun j hj => ?_⟩⟩
    obtain ⟨j', rfl⟩ := exists_eq_succ_of_ne_zero (show j ≠ 0 by intro x; subst x; simp at hj)
    exact (testBit_bit_succ _ _ _).trans (hk' _ (lt_of_succ_lt_succ hj))

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