image_tan_Ioo

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

The image of the open interval Ioo(-π/2, π/2) under tan is all real numbers.

Русский

Образ tan от открытого интервала Ioo(-π/2, π/2) равен всем вещественным числам.

LaTeX

$$$ \tan'' \mathrm{Ioo}\left(-\frac{\pi}{2}, \frac{\pi}{2}\right) = \mathbb{R} $$$

Lean4

theorem image_tan_Ioo : tan '' Ioo (-(π / 2)) (π / 2) = univ :=
  univ_subset_iff.1 surjOn_tan

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

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

Разделы

Аффилиация

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