lean_workbook_plus_78333

Open

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

Show that for $\theta_n \in (0, \frac{\pi}{2})$ , there exists a unique solution $\theta_{n+1} = \frac{1}{3}(\theta_{n} + \pi)$ on $(0, \frac{\pi}{2})$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78333 (n : ℕ) (θ_n : ℝ) (h₁ : 0 < θ_n ∧ θ_n < π/2) : ∃! θ_n1 : ℝ, θ_n1 = (θ_n + π)/3 ∧ 0 < θ_n1 ∧ θ_n1 < π/2   :=  by sorry

Source

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

View graph