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

trajectory_pos

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)

 114theorem trajectory_pos {f : ℝ → ℝ} (hf : RecognitionDescent f)
 115    {r : ℝ} (hr : 0 < r) (n : ℕ) : 0 < trajectory f r n := by

proof body

Term-mode proof.

 116  induction n with
 117  | zero => exact hr
 118  | succ k ih =>
 119      rw [trajectory_succ]
 120      exact hf.preserves_positive _ ih
 121

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.