tendsto_inv_nhdsGT_zero — Mathlib

English

If f tends to 0 from the right, then its reciprocal tends to +∞; i.e., Tendsto f l (nhdsWithin 0 (Ioi 0)) implies Tendsto f^{-1} l atTop.

Русский

Если f стремится к 0 справа, то 1/f стремится к +∞.

LaTeX

$$$\text{If } f \to 0^+ \text{ then } f^{-1} \to +\infty.$$$

Lean4

/-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/
theorem tendsto_inv_nhdsGT_zero : Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[>] (0 : 𝕜)) atTop :=
  inv_nhdsGT_zero.le

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