two_mul_arctan

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

← MathLib Explorer

English

For -1 < x < 1, 2 arctan x = arctan(2x/(1−x^2)).

Русский

Для -1 < x < 1: 2 arctan x = arctan(2x/(1−x^2)).

LaTeX

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

Lean4

theorem two_mul_arctan (h₁ : -1 < x) (h₂ : x < 1) : 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) := by
  rw [two_mul, arctan_add (by nlinarith)]; congr 1; ring

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

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

Разделы

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

Аффилиация

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