tendsto_norm_tan_atTop — Mathlib

English

For any k ∈ ℤ, as z approaches (2k+1)π/2 from within a punctured neighborhood, ||tan z|| tends to infinity.

Русский

Для любого k ∈ ℤ, при приближении z к (2k+1)π/2 из т.н. проколотого окрестного окружения, ||tan z|| стремится к бесконечности.

LaTeX

$$$$ \forall k \in \mathbb{Z}, \ \lim_{z \to (2k+1)\frac{\pi}{2}, z \neq (2k+1)\frac{\pi}{2}} |\tan z| = \infty. $$$$

Lean4

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

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