lean_workbook_plus_14911

Open

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

On the interval $\left[0,\dfrac{\pi}{2} \right], \sin x$ is strictly increasing and $\cos x$ is strictly decreasing.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14911 : ∀ x y : ℝ, x ∈ Set.Icc 0 (π / 2) ∧ y ∈ Set.Icc 0 (π / 2) → x < y → sin x < sin y ∧ cos y < cos x   :=  by sorry

Source