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

logicNatLift_unique_fun

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)

 102private theorem logicNatLift_unique_fun (B : PeanoObject)
 103    (f : PeanoObject.Hom logicNatPeano B) :
 104    f.toFun = (logicNatLift B).toFun := by

proof body

Tactic-mode proof.

 105  funext n
 106  induction n with
 107  | identity =>
 108      exact f.map_zero
 109  | step n ih =>
 110      calc
 111        f.toFun (LogicNat.step n) = B.step (f.toFun n) := f.map_step n
 112        _ = B.step ((logicNatLift B).toFun n) := by rw [ih]
 113        _ = (logicNatLift B).toFun (LogicNat.step n) := rfl
 114
 115/-- `LogicNat` is initial among Peano objects. -/

used by (2)

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

depends on (12)

Lean names referenced from this declaration's body.