antitoneOn_cos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

URI: https://scilib.ai/kg/mathlib#Real.antitoneOn_cos

English

For 0 ≤ x ≤ y ≤ π, cos y ≤ cos x.

Русский

Для 0 ≤ x ≤ y ≤ π косинус y не возрастает по отношению к x: cos y ≤ cos x.

LaTeX

$$$0 \le x \le y \le \pi \\Rightarrow \\cos y \le \cos x.$$$

Lean4

theorem antitoneOn_cos : AntitoneOn cos (Set.Icc 0 π) :=
  strictAntiOn_cos.antitoneOn

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru