English
In a densely ordered topological space with a minimal element absent, a half-open interval Ico(a,b) is a neighborhood of x precisely when x lies strictly between a and b.
Русский
В плотно упорядоченном топологическом пространстве без минимального элемента полуоткрытый интервал Ico(a,b) является окрестностью точки x тогда и только тогда, когда x расположен в интервале (a,b).
LaTeX
$$$Ico(a,b) \in \mathcal{N}(x) \iff x \in Ioo(a,b)$$$
Lean4
@[simp]
theorem Ico_mem_nhds_iff [NoMinOrder α] {a b x : α} : Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b := by
rw [← interior_Ico, mem_interior_iff_mem_nhds]