English
Let TopologicalSpace α be fixed. The local neighborhoods of the top element ⊤ in the extended real line EReal, restricted to points not equal to ⊤, correspond exactly to the image of the atTop filter under the real-to-EReal coe map.
Русский
Пусть задана топологическая пространство α. Окрестности точки ⊤ в расширенном вещественном числе EReal, взятые внутри множества {x ≠ ⊤}, совпадают с образованием фильтра atTop через отображение Real.toEReal.
LaTeX
$$$ 𝓝_{\neq}(\top) = (\mathrm{atTop}).\mathrm{map}(\mathrm{Real.toEReal}) $$$
Lean4
theorem nhdsWithin_top : 𝓝[≠] (⊤ : EReal) = (atTop).map Real.toEReal :=
by
apply (nhdsWithin_hasBasis nhds_top_basis_Ici _).ext (atTop_basis.map Real.toEReal)
· simp only [EReal.image_coe_Ici, true_and]
intro x hx
by_cases hx_bot : x = ⊥
· simp [hx_bot]
lift x to ℝ using ⟨hx.ne_top, hx_bot⟩
refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
simp [h1, h2.ne_top]
· simp only [EReal.image_coe_Ici, true_implies]
refine fun x ↦ ⟨x, ⟨EReal.coe_lt_top x, fun x ⟨(h1 : _ ≤ x), h2⟩ ↦ ?_⟩⟩
simp [h1, Ne.lt_top' fun a ↦ h2 a.symm]
