arctan_tan

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

For x with -π/2 < x < π/2, arctan(tan x) = x.

Русский

Для x с -π/2 < x < π/2, arctan(tan x) = x.

LaTeX

$$$ \arctan(\tan x) = x \quad \text{if } -\frac{\pi}{2} < x < \frac{\pi}{2} $$$

Lean4

theorem arctan_tan (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) : arctan (tan x) = x :=
  Subtype.ext_iff.1 <| tanOrderIso.symm_apply_apply ⟨x, hx₁, hx₂⟩

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

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

Разделы

Аффилиация

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