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

logicNat_NNO_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)

  27theorem logicNat_NNO_uniqueness :
  28    ∀ {α : Type*} (base : α) (step : α → α)
  29      (f g : LogicNat → α),
  30      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
  31      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
  32      f = g :=

proof body

Term-mode proof.

  33  @nno_universal_uniqueness
  34

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.