lean_workbook_plus_64007

Proved

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

For $\frac{1}{5}\leq{x_n}\leq{1}$ , $\implies{x_{n+1}=\frac{1}{5}(x_{n}^3+\frac{1}{x_n})<\frac{1+5}{5}<2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64007 (x : ℝ) (hx: 1/5 ≤ x ∧ x ≤ 1) : 1/5 * (x^3 + 1/x) < 2   :=  by sorry

Source