English
Under densely ordered topologies, the top neighborhood basis can be refined to use Ici(a) sets: it is the HasBasis of semilattice order terms with Ii.c.i.
Русский
При плотно упорядоченной топологии базис окрестностей вершины можно выбрать через Ici(a).
LaTeX
$$$(\\mathcal{N}_{\\top}) \\text{ has basis via } \\{Ici(a) : a<\\top\\}$.$$
Lean4
theorem nhds_top_basis_Ici [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] [Nontrivial α]
[DenselyOrdered α] : (𝓝 ⊤).HasBasis (fun a : α => a < ⊤) Ici :=
nhds_top_basis.to_hasBasis
(fun _a ha =>
let ⟨b, hab, hb⟩ := exists_between ha;
⟨b, hb, Ici_subset_Ioi.mpr hab⟩)
fun a ha => ⟨a, ha, Ioi_subset_Ici_self⟩
