Prove2Me

lean_workbook_plus_52484

Open

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

Studying the function f:[−π2,π2]→R f:\left[-\frac{\pi}{2},\frac{\pi}{2}\right]\to\mathbb R , f(x)=sin2(x)+cos(x)−54 f(x) = sin^{2}(x)+cos(x)-\frac{5}{4} we get that f(x)≤0 f(x)\leq 0 ∀x∈[−π2,π2] \forall x\in\left[-\frac{\pi}{2},\frac{\pi}{2}\right]

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52484 :
  ∀ x ∈ Set.Icc (-Real.pi / 2) (Real.pi / 2), (Real.sin x)^2 + Real.cos x - 5 / 4 ≤ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph