Prove2Me

Bounds for twice the sine-cosine product

Proved
WorkbookSource.problem_11845

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Given 0<x<π/20<x<\pi/2 ; we see that 0≤sin⁡(2x)≤1  ⟹  0≤2sin⁡x cos⁡x≤1 0 \le \sin (2x) \le 1 \implies 0 \le 2 \sin x \ \cos x \le 1

Source: InternLM Lean-Workbook, record lean_workbook_11845 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_11845 : ∀ x : ℝ, 0 < x ∧ x < π/2 → 0 ≤ 2 * Real.sin x * Real.cos x ∧ 2 * Real.sin x * Real.cos x ≤ 1  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_11845; Apache-2.0

View graph