evenOddRec_odd — Mathlib

English

For all n, the value at 2n+1 is obtained by applying the odd step to n.

Русский

Для каждого n значение на 2n+1 получаем через этап для нечётного числа.

LaTeX

$$$$ (2n+1).evenOddRec\ h0\ h_{even}\ h_{odd} = h_{odd} n\ (evenOddRec\ h0\ h_{even}\ h_{odd} n). $$$$

Lean4

@[simp]
theorem evenOddRec_odd {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i)) (h_odd : ∀ i, P i → P (2 * i + 1))
    (H : h_even 0 h0 = h0) (n : ℕ) : (2 * n + 1).evenOddRec h0 h_even h_odd = h_odd n (evenOddRec h0 h_even h_odd n) :=
  by
  apply binaryRec_eq true n
  simp [H]

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