tendsto_norm_tan_of_cos_eq_zero — Mathlib

English

If cos x = 0, then ||tan z|| tends to infinity as z → x with z ≠ x.

Русский

Если cos x = 0, то ||tan z|| неограничен при сближении z к x с z ≠ x, т.е. стремится к бесконечности.

LaTeX

$$$$ \text{If } \cos x = 0, \quad \lim_{z \to x, z \neq x} \|\tan z\| = \infty. $$$$

Lean4

theorem tendsto_norm_tan_of_cos_eq_zero {x : ℂ} (hx : cos x = 0) : Tendsto (fun x => ‖tan x‖) (𝓝[≠] x) atTop :=
  by
  simp only [tan_eq_sin_div_cos, norm_div]
  have A : sin x ≠ 0 := fun h => by simpa [*, sq] using sin_sq_add_cos_sq x
  have B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0) := hx ▸ (hasDerivAt_cos x).tendsto_nhdsNE (neg_ne_zero.2 A)
  exact
    continuous_sin.continuousWithinAt.norm.pos_mul_atTop (norm_pos_iff.2 A)
      (tendsto_norm_nhdsNE_zero.comp B).inv_tendsto_nhdsGT_zero

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