nhds_basis_Ioo — Mathlib

English

Specialized basis: neighborhoods of a are generated by intervals Ioo(l,u) with l<a<u.

Русский

Уточненный базис: окрестности a формируются интервалами Ioo(l,u) с l<a<u.

LaTeX

$$$(\\nhds a).HasBasis (l,u)\\;:\\; l

Lean4

theorem nhds_basis_Ioo [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] (a : α) :
    (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2 :=
  nhds_basis_Ioo' (exists_lt a) (exists_gt a)

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