nhds_bot_basis — Mathlib

English

Analogous bottom basis: the bottom neighborhood basis is derived from the dual of the top basis.

Русский

Аналогичный нижний базис: базис окрестностей нуля выводится через двойственный верхний базис.

LaTeX

$$$𝓝(\\bot)\\text{ has basis from the dual construction.}$$$

Lean4

theorem nhds_bot_basis [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] [Nontrivial α] :
    (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) fun a : α => Iio a :=
  nhds_top_basis (α := αᵒᵈ)

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