arctan_inv_of_neg

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

← MathLib Explorer

English

For x < 0, arctan(x^{-1}) = -(π/2) − arctan x.

Русский

Для x < 0: arctan(1/x) = −(π/2) − arctan x.

LaTeX

$$$\\\\arctan(x^{-1}) = -\\\\frac{\\\\pi}{2} - \\\\arctan x \\\\quad (x<0).$$$

Lean4

theorem arctan_inv_of_neg (h : x < 0) : arctan x⁻¹ = -(π / 2) - arctan x :=
  by
  have := arctan_inv_of_pos (neg_pos.mpr h)
  rwa [inv_neg, arctan_neg, neg_eq_iff_eq_neg, neg_sub', arctan_neg, neg_neg] at this

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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