binaryRec_one — Mathlib

English

If we evaluate the binary-recursion at 1, we get bit true 0 zero.

Русский

Если вычислить бинарную рекурсию в аргументе 1, получаем bit true 0 zero.

LaTeX

$$$ binaryRec\ (zero)\ (bit)\ 1 = bit\ true\ 0\ zero $$$

Lean4

@[simp]
theorem binaryRec_one (zero : motive 0) (bit : ∀ b n, motive n → motive (bit b n)) :
    binaryRec (motive := motive) zero bit 1 = bit true 0 zero :=
  by
  rw [binaryRec]
  simp only [add_one_ne_zero, ↓reduceDIte, Nat.reduceShiftRight, binaryRec_zero]
  rfl

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