tendsto_abs_tan_of_cos_eq_zero — Mathlib

English

If cos x = 0, then as x approaches x from any punctured neighborhood, abs(tan x) tends to infinity.

Русский

Если cos x = 0, то при подходе к точке x с удалением самой точки из окружности, |tan x| стремится к бесконечности.

LaTeX

$$$ \cos x = 0 \Rightarrow \operatorname{Tendsto} (|\tan t|) (\mathcal{nhdsWithin}(x, \mathbb{R} \setminus \{x\})) \\text{atTop}. $$$

Lean4

theorem tendsto_abs_tan_of_cos_eq_zero {x : ℝ} (hx : cos x = 0) : Tendsto (fun x => abs (tan x)) (𝓝[≠] x) atTop :=
  by
  have hx : Complex.cos x = 0 := mod_cast hx
  simp only [← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_tan]
  refine (Complex.tendsto_norm_tan_of_cos_eq_zero hx).comp ?_
  refine Tendsto.inf Complex.continuous_ofReal.continuousAt ?_
  exact tendsto_principal_principal.2 fun y => mt Complex.ofReal_inj.1

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