Theorems · Definition · order theory

Nat.leRec

{n : ℕ} →
  {motive : (m : ℕ) → n ≤ m → Sort u_1} →
    motive n ⋯ → (⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) → {m : ℕ} → (h : n ≤ m) → motive m h

Recursion starting at a non-zero number: given a map C k → C (k+1) for each k ≥ n, there is a map from C n to each C m, n ≤ m. This is a version of Nat.le.rec that works for Sort u. Similarly to Nat.le.rec, it can be used as `` induction hle using Nat.leRec with | refl => sorry | le_succ_of_le hle ih => sorry ``

Defined in

Mathlib.Data.Nat.Init

Cited by

13 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms