hasBasis_nhds_Ioc — Mathlib

English

Under OrderTopology and PredOrder with NoMaxOrder, the neighborhood filter at a has a basis given by right-closed intervals Ico(a, x) for x > a.

Русский

При OrderTopology и PredOrder с NoMaxOrder окрестности a имеют базис из интервалов Ico(a, x) для x > a.

LaTeX

$$$(\\\\mathcal{N}(a)).HasBasis (a < \\\\cdot) (Set.Ico(a, \\\\cdot))$$

Lean4

theorem hasBasis_nhds_Ioc [OrderTopology α] [PredOrder α] [NoMaxOrder α] {a : α} :
    (𝓝 a).HasBasis (a < ·) (Set.Ico a ·) :=
  PredOrder.hasBasis_nhds_Ioc_of_exists_gt (exists_gt a)

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