range_arctan

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

If -π/2 < x < π/2, then arctan(tan x) = x.

Русский

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

LaTeX

$$$ x \in \left(-\frac{\pi}{2}, \frac{\pi}{2}\right) \Rightarrow \arctan(\tan x) = x $$$

Lean4

@[simp]
theorem range_arctan : range arctan = Ioo (-(π / 2)) (π / 2) :=
  ((EquivLike.surjective _).range_comp _).trans Subtype.range_coe

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

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

Разделы

Аффилиация

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