lean_workbook_plus_32152

Open

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

Given $0<x<\pi/2$ ; we see that $0 \le \sin (2x) \le 1 \implies 0 \le 2 \sin x \ \cos x \le 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32152 : ∀ x ∈ Set.Ioo 0 (Real.pi / 2), 0 ≤ 2 * Real.sin x * Real.cos x ∧ 2 * Real.sin x * Real.cos x ≤ 1   :=  by sorry

Source