English
Let TopologicalSpace α be fixed. The neighborhood filter at the bottom element ⊥ in EReal, restricted to points not equal to ⊥, is exactly the image of the atBot filter under Real.toEReal.
Русский
Пусть задана топологическая пространство α. Окрестности точки ⊥ в EReal, взятые внутри множества {x ≠ ⊥}, совпадают с образованием фильтра atBot через отображение Real.toEReal.
LaTeX
$$$ 𝓝_{\neq}(\bot) = (\mathrm{atBot}).\mathrm{map}(\mathrm{Real.toEReal}) $$$
Lean4
theorem nhdsWithin_bot : 𝓝[≠] (⊥ : EReal) = (atBot).map Real.toEReal :=
by
apply (nhdsWithin_hasBasis nhds_bot_basis_Iic _).ext (atBot_basis.map Real.toEReal)
· simp only [EReal.image_coe_Iic, true_and]
intro x hx
by_cases hx_top : x = ⊤
· simp [hx_top]
lift x to ℝ using ⟨hx_top, hx.ne_bot⟩
refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
simp [h2, h1.ne_bot]
· simp only [EReal.image_coe_Iic, true_implies]
refine fun x ↦ ⟨x, ⟨EReal.bot_lt_coe x, fun x ⟨(h1 : x ≤ _), h2⟩ ↦ ?_⟩⟩
simp [h1, Ne.bot_lt' fun a ↦ h2 a.symm]
