mem_nhds_iff_exists_Ioo_subset — Mathlib

English

In an OrderTopology α with NoMaxOrder and NoMinOrder, a set s is a neighborhood of a iff there exist l<u with a∈Ioo(l,u) and Ioo(l,u)⊆s.

Русский

В OrderTopology α с отсутствием максимумa и минимума окрестность s точки a эквивалентна существованию l<u с a∈Ioo(l,u) и Ioo(l,u)⊆s.

LaTeX

$$$s\\in 𝓝 a \\iff \\exists l,u (a\\in Ioo(l,u) \\land Ioo(l,u)\\subseteq s)$$$

Lean4

/-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`.
-/
theorem mem_nhds_iff_exists_Ioo_subset [OrderTopology α] [NoMaxOrder α] [NoMinOrder α] {a : α} {s : Set α} :
    s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s :=
  mem_nhds_iff_exists_Ioo_subset' (exists_lt a) (exists_gt a)

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