inv_nhdsLT_zero — Mathlib

English

In an ordered topological field, the reciprocal of the left-neighborhood of zero tends to minus infinity: (𝓝[<](0))^{-1} = atBot.

Русский

В упорядоченном топологическом поле обратное к окрестности слева от нуля расходится к минус бесконечности: (𝓝[<](0))^{-1} = atBot.

LaTeX

$$$\big(\nhds_{<0}(0)\big)^{-1} = \mathrm{atBot}$$$

Lean4

@[simp]
theorem inv_nhdsLT_zero : (𝓝[<] (0 : 𝕜))⁻¹ = atBot := by rw [← inv_atBot₀, inv_inv]

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