strictAntiOn_arccos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

arccos is strictly decreasing on the interval [-1,1].

Русский

Арккосинус строго убывает на отрезке [-1,1].

LaTeX

$$∀ a,b ∈ [-1,1], a < b ⇒ \arccos a > \arccos b$$

Lean4

theorem strictAntiOn_arccos : StrictAntiOn arccos (Icc (-1) 1) := fun _ hx _ hy h =>
  sub_lt_sub_left (strictMonoOn_arcsin hx hy h) _

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

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

Разделы

Аффилиация

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