Dividing a strict angle bound
ProvedWorkbookSource.problem_49585lean-workbooksource-checked
Given the restriction , find the valid range for .
Source: InternLM Lean-Workbook, record lean_workbook_49585 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_49585 (x : ℝ) (h : 3 * x < π) : x < π / 3 := by sorry
Source