Prove2Me

lean_workbook_plus_11519

Proved

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

Then a2−a1≥t,a3−a1≥2t,...,an−a1≥(n−1)ta_2-a_1 \geq t, a_3-a_1 \geq 2t,...,a_n-a_1 \geq (n-1)t

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11519 (n : ℕ) (a : ℕ → ℝ) (t : ℝ) (h₁ : ∀ i, a (i + 1) - a i ≥ t) : ∀ i, a (i + 1) - a 1 ≥ i * t   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph