Lean-Workbook Plus 13487: Trigonometric inequality

Proved

WorkbookRestored.plus_13487

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For every real $x$ , $\tfrac14\le\cos^6 x+\sin^6 x\le1$ .

Source: Lean-Workbook row lean_workbook_plus_13487 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real

Formal statement

theorem WorkbookRestored.plus_13487 :
  ∀ x : ℝ, 1 / 4 ≤ cos x ^ 6 + sin x ^ 6 ∧ cos x ^ 6 + sin x ^ 6 ≤ 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_13487; immutable original Prove2Me node 4c62a07d-1a9a-424f-8b41-f2f77582c4b2

View graph