Prove2Me

Shape_of_Cosine_Function

Proved

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

analysismonotonicityproofwikitrigonometry

The cosine function is strictly decreasing on [0, pi].

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

theorem Shape_of_Cosine_Function : StrictAntiOn Real.cos (Set.Icc 0 Real.pi) := by sorry
Source
https://proofwiki.org/wiki/Shape_of_Cosine_Function

View graph