evenOddRec_even — Mathlib

English

For all n, the value at 2n is obtained by applying the even step to n.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem evenOddRec_even {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).evenOddRec h0 h_even h_odd = h_even n (evenOddRec h0 h_even h_odd n) :=
  by
  apply binaryRec_eq false n
  simp [H]

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