tendsto_inv_nhdsLT_zero — Mathlib

English

Let 𝕜 be an ordered field with its standard topology. Then as x approaches 0 from the left, x^{-1} tends to −∞.

Русский

Пусть 𝕜 — упорядоченное поле с обычной топологией. Тогда при подходе x к 0 слева x^{-1} стремится к −∞.

LaTeX

$$$\lim_{x \to 0^-} x^{-1} = -\infty$$$

Lean4

/-- The function `x ↦ x⁻¹` tends to `-∞` on the left of `0`. -/
theorem tendsto_inv_nhdsLT_zero : Tendsto (fun x : 𝕜 => x⁻¹) (𝓝[<] (0 : 𝕜)) atBot :=
  inv_nhdsLT_zero.le

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