surjOn_tan — Mathlib

English

The function tan is surjective from the interval Ioo(-π/2, π/2) onto all real numbers.

Русский

Функция tan образует всю множество действительных чисел при ограничении на интервал Ioo(-π/2, π/2).

LaTeX

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

Lean4

theorem surjOn_tan : SurjOn tan (Ioo (-(π / 2)) (π / 2)) univ :=
  have := neg_lt_self pi_div_two_pos
  continuousOn_tan_Ioo.surjOn_of_tendsto (nonempty_Ioo.2 this)
    (by rw [tendsto_comp_coe_Ioo_atBot this]; exact tendsto_tan_neg_pi_div_two)
    (by rw [tendsto_comp_coe_Ioo_atTop this]; exact tendsto_tan_pi_div_two)

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