Theorems · Definition · order theory

Nat.leRecOn

{C : ℕ → Sort u_1} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m

Recursion starting at a non-zero number: given a map C k → C (k + 1) for each k, there is a map from C n to each C m, n ≤ m. For a version where the assumption is only made when k ≥ n, see Nat.leRec.

Defined in

Mathlib.Data.Nat.Init

Cited by

13 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms