hasBasis_nhds_Ioc — Mathlib

English

For OrderTopology α, SuccOrder α, and NoMinOrder α, the neighborhood basis at a is given by sets Ioc(x, a) with x < a.

Русский

Для OrderTopology α, SuccOrder α и NoMinOrder α базис окрестностей a задаётся множеством Ioc(x,a) при x<a.

LaTeX

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

Lean4

theorem hasBasis_nhds_Ioc [OrderTopology α] [SuccOrder α] {a : α} [NoMinOrder α] :
    (𝓝 a).HasBasis (· < a) (Set.Ioc · a) :=
  SuccOrder.hasBasis_nhds_Ioc_of_exists_lt (exists_lt a)

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