lean_workbook_plus_16433

Proved

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

Is the statement correct? In the range $2/3<x<1$ , we always have $\frac{1-x}{1+3x}<\frac{1}{3}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16433 (x : ℝ) (h₁ : (2:ℝ)/3 < x) (h₂ : x < 1) : (1 - x) / (1 + 3 * x) < 1 / 3   :=  by sorry

Source