arctan_eq_of_tan_eq

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

← MathLib Explorer

English

If tan x = y and x lies in (-π/2, π/2), then arctan y = x.

Русский

Если tan x = y и x ∈ (-π/2, π/2), то arctan y = x.

LaTeX

$$$ (\tan x = y) \\land ( -\\frac{\\pi}{2} < x < \\frac{\\pi}{2} ) \\Rightarrow \\arctan y = x $$$

Lean4

theorem arctan_eq_of_tan_eq (h : tan x = y) (hx : x ∈ Ioo (-(π / 2)) (π / 2)) : arctan y = x :=
  injOn_tan (arctan_mem_Ioo _) hx (by rw [tan_arctan, h])

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

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

Разделы

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

Аффилиация

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