Continuous iteration above the identity diverges to infinity
ProvedWorkbookCorrected.plus_65496corrected-formalizationlean-workbooksequencessource-checked
Let f:ℝ→ℝ be continuous, with f(x)>x for every x≥0. Define u₀=0 and uₙ₊₁=f(uₙ). Then uₙ tends to positive infinity.
Formalization Note: Restores the source’s continuity assumption, omitted in the original formalization.
Source: InternLM Lean-Workbook, record lean_workbook_plus_65496 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_65496 (f : ℝ → ℝ) (hc : Continuous f) (hf : ∀ x : ℝ, 0 ≤ x → x < f x) (u : ℕ → ℝ) (u0 : u 0 = 0) (hu : ∀ n : ℕ, u (n+1)=f (u n)) : ∀ M : ℝ, ∃ N : ℕ, ∀ n : ℕ, N ≤ n → M < u n := by sorry
Source