mem_nhds_iff_exists_Ioo_subset' — Mathlib

English

For any a with l<a and a< u, the neighborhoods of a have a basis consisting of intervals Ioo(l, u).

Русский

Для любой точки a, лежащей между l и u, базис окрестностей состоит из интервалов Ioo(l,u).

LaTeX

$$$\\ (\\mathcal{N}_a)\\text{ HasBasis }(b\\mapsto b_1

Lean4

/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`,
provided `a` is neither a bottom element nor a top element. -/
theorem mem_nhds_iff_exists_Ioo_subset' [OrderTopology α] {a : α} {s : Set α} (hl : ∃ l, l < a) (hu : ∃ u, a < u) :
    s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s := by
  constructor
  · intro h
    rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩
    rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩
    exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩
  · rintro ⟨l, u, ha, h⟩
    apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h

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