lean_workbook_plus_43176

Open

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

If $m\in[-1,1]$ then put $m=sin(\theta)$ where $\theta\in[-\pi/2,\pi/2]$ . Thus $cos(\theta)\geq{0}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43176 : ∀ m : ℝ, m ∈ Set.Icc (-1) 1 → ∃ θ : ℝ, θ ∈ Set.Icc (-Real.pi/2) (Real.pi/2) ∧ m = Real.sin θ   :=  by sorry

Source