nhds_bot_basis_Iic — Mathlib

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 (α := αᵒᵈ)

Похожие утверждения