arctan_lt_arctan

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

For any real x < y, arctan x < arctan y.

Русский

Для любых x < y выполняется arctan x < arctan y.

LaTeX

$$$\\forall x

Lean4

@[gcongr]
theorem arctan_lt_arctan (hxy : x < y) : arctan x < arctan y :=
  arctan_strictMono hxy

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

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

Разделы

Аффилиация

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