Theorems · Definition · number theory

Nat.evenOddRec

{P : ℕ → Sort u_1} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n

Recursion principle on even and odd numbers: if we have P 0, and for all i : ℕ we can extend from P i to both P (2 * i) and P (2 * i + 1), then we have P n for all n : ℕ. This is nothing more than a wrapper around Nat.binaryRec, to avoid having to switch to dealing with bit0 and bit1.

Defined in

Mathlib.Data.Nat.EvenOddRec

Cited by

3 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Quot.sound