lean_workbook_plus_49326

Open

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

We know that $\tan{\theta}$ is increasing and $> 0$ for $\theta\in(0,\frac{\pi}{2}).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49326 : ∀ θ : ℝ, θ ∈ Set.Ioo 0 (Real.pi / 2) → 0 < Real.tan θ   :=  by sorry

Source