invQParam_tendsto — Mathlib

English

If h > 0, invQParam(h, z) tends to infinity as z approaches 0 along the punctured neighborhood.

Русский

Если h > 0, invQParam(h, z) стремится к бесконечности при приближении z к 0 вдоль окружности без 0.

LaTeX

$$hh > 0 ⇒ Tendsto (invQParam h) (𝓝[≠] 0) I∞$$

Lean4

theorem invQParam_tendsto (hh : 0 < h) : Tendsto (invQParam h) (𝓝[≠] 0) I∞ :=
  by
  simp only [tendsto_comap_iff, comp_def, im_invQParam]
  apply Tendsto.const_mul_atBot_of_neg (div_neg_of_neg_of_pos (neg_lt_zero.mpr hh) (by positivity))
  exact Real.tendsto_log_nhdsGT_zero.comp tendsto_norm_nhdsNE_zero

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