hasBasis_nhds_Ioc_of_exists_gt — Mathlib

English

Let α be a densely ordered linear order with the order topology and PredOrder structure. If there exists a > a, then the neighborhoods of a have a basis consisting of right-closed-open intervals [a, t) with t > a.

Русский

Пусть α—упорядоченное линейное множество с топологией порядка иPredOrder. Если существует u > a, окрестности точки a образуют базис из интервалов [a, t) с t > a.

LaTeX

$$$(\\\\mathcal{N}(a)) \\\\text{ has basis } \\\\{ [a, t) \\\\mid a < t \\\\}$$$

Lean4

theorem hasBasis_nhds_Ioc_of_exists_gt [OrderTopology α] [PredOrder α] {a : α} (ha : ∃ u, a < u) :
    (𝓝 a).HasBasis (a < ·) (Set.Ico a ·) :=
  PredOrder.nhdsGE_eq_nhds a ▸ nhdsGE_basis_of_exists_gt ha

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