tendsto_abs_tan_atTop — Mathlib

English

For every integer k, abs(tan x) tends to infinity as x approaches (2k+1)π/2 from any punctured neighborhood.

Русский

Для каждого целого k |tan x| стремится к бесконечности при подходе к (2k+1)π/2 не достигая самой точки.

LaTeX

$$$ \forall k \in \mathbb{Z}, \; \operatorname{Tendsto} (|\tan x|) (\mathcal{nhdsWithin}((2k+1)\pi/2)) \text{atTop}. $$$

Lean4

theorem tendsto_abs_tan_atTop (k : ℤ) : Tendsto (fun x => abs (tan x)) (𝓝[≠] ((2 * k + 1) * π / 2)) atTop :=
  tendsto_abs_tan_of_cos_eq_zero <| cos_eq_zero_iff.2 ⟨k, rfl⟩

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