English
Analogous statement for the bottom with a dual arrangement and dense ordering: the bottom neighborhood basis is derived from Iic sets.
Русский
Аналогично для низа: базис окрестностей низа выводится из Iic-множеств при плотном порядке.
LaTeX
$$$(\\mathcal{N}_{\\bot}) \\text{ has basis via } Iic$.$$
Lean4
theorem nhds_bot_basis_Iic [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α]
[DenselyOrdered α] : (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) Iic :=
nhds_top_basis_Ici (α := αᵒᵈ)