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

isInitial

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)

  68def isInitial (h : IsNaturalNumberObject z s) :
  69    PeanoObject.IsInitial (toPeano h) where
  70  lift := fun B =>

proof body

Definition body.

  71    { toFun := h.recursor B.zero B.step
  72      map_zero := h.recursor_zero B.zero B.step
  73      map_step := fun n => h.recursor_step B.zero B.step n }
  74  uniq := by
  75    intro B f g
  76    funext n
  77    have hf := h.recursor_unique B.zero B.step f.toFun f.map_zero f.map_step n
  78    have hg := h.recursor_unique B.zero B.step g.toFun g.map_zero g.map_step n
  79    rw [hf, hg]
  80
  81end IsNaturalNumberObject
  82
  83/-! ## `LogicNat` is a natural-number object -/
  84
  85/-- `LogicNat` with `identity` and `step` is a Lawvere natural-number object. -/

depends on (15)

Lean names referenced from this declaration's body.