pith. machine review for the scientific record. sign in
theorem proved term proof

nno_universal_uniqueness

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)

  82theorem nno_universal_uniqueness {α : Type*} (base : α) (step : α → α)
  83    (f g : LogicNat → α)
  84    (hf_zero : f LogicNat.zero = base)
  85    (hf_succ : ∀ n, f (LogicNat.succ n) = step (f n))
  86    (hg_zero : g LogicNat.zero = base)
  87    (hg_succ : ∀ n, g (LogicNat.succ n) = step (g n)) :
  88    f = g := by

proof body

Term-mode proof.

  89  funext n
  90  induction n with
  91  | identity =>
  92      rw [show LogicNat.identity = LogicNat.zero from rfl, hf_zero, hg_zero]
  93  | step k ih =>
  94      rw [show LogicNat.step k = LogicNat.succ k from rfl, hf_succ k, hg_succ k, ih]
  95
  96/-! ## Master cert -/
  97

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.