hasBasis_nhds_Ioc_of_exists_lt — Mathlib

English

In an OrderTopology with SuccOrder and NoMinOrder, the neighborhoods of a have a basis consisting of right-intervals Ioc(·, a).

Русский

В OrderTopology с SuccOrder и NoMinOrder окрестности a образуют базис из интервалов Ioc(x, a).

LaTeX

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

Lean4

theorem hasBasis_nhds_Ioc_of_exists_lt [OrderTopology α] [SuccOrder α] {a : α} (ha : ∃ l, l < a) :
    (𝓝 a).HasBasis (· < a) (Set.Ioc · a) :=
  SuccOrder.nhdsLE_eq_nhds a ▸ nhdsLE_basis_of_exists_lt ha

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