arctan_mem_Ioo

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

The range of arctan is the open interval (-π/2, π/2).

Русский

Область значений arctan = (-π/2, π/2).

LaTeX

$$$ \operatorname{range}(\arctan) = \mathrm{Ioo}\left(-\frac{\pi}{2}, \frac{\pi}{2}\right) $$$

Lean4

theorem arctan_mem_Ioo (x : ℝ) : arctan x ∈ Ioo (-(π / 2)) (π / 2) :=
  Subtype.coe_prop _

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

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

Разделы

Аффилиация

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