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

induction

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)

 106theorem induction
 107    {motive : LogicNat → Prop}
 108    (h0 : motive zero)
 109    (hs : ∀ n, motive n → motive (succ n)) :
 110    ∀ n, motive n := by

proof body

Term-mode proof.

 111  intro n
 112  induction n with
 113  | identity => exact h0
 114  | step n ih => exact hs n ih
 115
 116/-! ## 4. Addition and Multiplication
 117
 118Addition is repeated successor; multiplication is repeated addition.
 119Both are defined by recursion on the second argument. We register
 120them as `Add` and `Mul` instances so Lean's standard `+` and `*`
 121notation work on `LogicNat` directly. -/
 122
 123/-- Addition by recursion on the second argument. -/

depends on (12)

Lean names referenced from this declaration's body.