lean_workbook_plus_19379

Open

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

Results $1\le 2-\sin x+\cos x\le 3, \forall x\in\left[0,\dfrac{\pi}{2} \right]\Longrightarrow$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19379 (x: ℝ) (hx: 0 ≤ x ∧ x ≤ π/2) :
  1 ≤ 2 - Real.sin x + Real.cos x ∧ 2 - Real.sin x + Real.cos x ≤ 3   :=  by sorry

Source