inv_atTop₀ — Mathlib

English

In a linearly ordered field, the reciprocal map sends the neighborhood basis to infinity: the inverse of the atTop filter equals the nhds of +∞ from the right of zero; i.e., (atTop)^{-1} = nhds[>](0).

Русский

В линейно упорядоченном поле отображение обратного значения переводит окрестности к +∞; то есть (atTop)^{-1} = nhds[>](0).

LaTeX

$$$(\operatorname{atTop})^{-1} = \mathcal{N}_{[>0]}(0).$$$

Lean4

@[simp]
theorem inv_atTop₀ : (atTop : Filter 𝕜)⁻¹ = 𝓝[>] 0 :=
  (((atTop_basis_Ioi' (0 : 𝕜)).map _).comp_surjective inv_surjective).eq_of_same_basis <|
    (nhdsGT_basis _).congr (by simp) fun a ha ↦ by simp [inv_Ioi₀ (inv_pos.2 ha)]

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