English
There exists a point below the top; the top neighborhood basis can be obtained from the lower basis by a duality argument.
Русский
Существуют точки ниже вершины; базис окрестностей вершины получается из нижнего базиса через дуальное преобразование.
LaTeX
$$$(\\exists x: α,\; x<\\top) \\Rightarrow 𝓝(\\top)\\text{ has basis from } Ioi/related.$$$
Lean4
theorem nhds_top_basis [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α] :
(𝓝 ⊤).HasBasis (fun a : α => a < ⊤) fun a : α => Ioi a :=
by
have : ∃ x : α, x < ⊤ := (exists_ne ⊤).imp fun x hx => hx.lt_top
simpa only [Iic_top, nhdsWithin_univ, Ioc_top] using nhdsLE_basis_of_exists_lt this
