pith. machine review for the scientific record. sign in
structure definition def or abbrev

IsNaturalNumberObject

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  49structure IsNaturalNumberObject {N : Type u} (z : N) (s : N → N) where
  50  recursor : ∀ {X : Type u}, X → (X → X) → N → X
  51  recursor_zero : ∀ {X : Type u} (x : X) (f : X → X), recursor x f z = x
  52  recursor_step : ∀ {X : Type u} (x : X) (f : X → X) (n : N),
  53    recursor x f (s n) = f (recursor x f n)
  54  recursor_unique : ∀ {X : Type u} (x : X) (f : X → X) (h : N → X),
  55    h z = x → (∀ n, h (s n) = f (h n)) → ∀ n, h n = recursor x f n
  56
  57namespace IsNaturalNumberObject
  58
  59variable {N : Type u} {z : N} {s : N → N}
  60
  61/-- The Peano object carried by a natural-number object. -/

used by (14)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.