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

canonical_peanoSurface

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)

 242theorem canonical_peanoSurface (R : LogicRealization) :
 243    PeanoSurface (canonical R) where
 244  zero_ne_step := by

proof body

Tactic-mode proof.

 245    intro x h
 246    cases h
 247  step_injective := by
 248    intro a b h
 249    exact LogicNat.succ_injective h
 250  induction := by
 251    intro P h0 hstep n
 252    exact LogicNat.induction (motive := P) h0 hstep n
 253
 254end ArithmeticOf
 255
 256end Foundation
 257end IndisputableMonolith

depends on (8)

Lean names referenced from this declaration's body.