lean_workbook_plus_25841

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Does the statement 'there exists $k$ such that for all $n \ge k$ , $f(n) \ge \frac{1}{2}$ ' hold for a function $f(n)$ that converges to 1 as $n$ approaches infinity?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25841 (f : ℕ → ℝ) (h : ∀ ε : ℝ, ε > 0 → ∃ N : ℕ, ∀ n : ℕ, n ≥ N → |f n - 1| < ε) : ∃ k : ℕ, ∀ n : ℕ, n ≥ k → f n ≥ 1 / 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph