antitone_arccos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

arccos is an antitone function on ℝ.

Русский

Арккосинус антимонотонна на всей области определения.

LaTeX

$$Antitone( arccos )$$

Lean4

theorem antitone_arccos : Antitone arccos := fun _ _ ↦ arccos_le_arccos

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

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

Разделы

Аффилиация

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