nhds_basis_Ioo' — Mathlib

English

For an OrderTopology α, there exist neighborhoods of a that are precisely the unions of intervals Ioo(l,u) with l<a<u.

Русский

В OrderTopology α существуют окрестности точки a, которые равны объединениям интервалов Ioo(l,u) с l<a<u.

LaTeX

$$$(\\nhds a)\\;\\text{HasBasis }(l,u)\\;\\text{for }l

Lean4

theorem nhds_basis_Ioo' [OrderTopology α] {a : α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) :
    (𝓝 a).HasBasis (fun b : α × α => b.1 < a ∧ a < b.2) fun b => Ioo b.1 b.2 :=
  ⟨fun s => (mem_nhds_iff_exists_Ioo_subset' hl hu).trans <| by simp⟩

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