Theorems · Definition · number theory

Nat.binaryRec

{motive : ℕ → Sort u} → motive 0 → ((b : Bool) → (n : ℕ) → motive n → motive (Nat.bit b n)) → (n : ℕ) → motive n

A recursion principle for bit representations of natural numbers. For a predicate motive : Nat → Sort u, if instances can be constructed for natural numbers of the form bit b n, they can be constructed for all natural numbers.

Defined in

Mathlib.Data.Nat.BinaryRec

Cited by

24 results in Mathlib

Foundations

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