two_mul_arctan_sub_pi

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

← MathLib Explorer

English

If x < −1, then 2 arctan x = arctan(2x/(1−x^2)) − π.

Русский

Если x < −1, то 2 arctan x = arctan(2x/(1−x^2)) − π.

LaTeX

$$$x < -1 \\Rightarrow 2 \\arctan x = \\arctan\\\\left(\\\\frac{2x}{1-x^2}\\\\right) - π.$$$

Lean4

theorem two_mul_arctan_sub_pi (h : x < -1) : 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) - π := by
  rw [two_mul, arctan_add_eq_sub_pi (by nlinarith) (by linarith)]; congr 2; ring

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

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

Разделы

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

Аффилиация

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