Ico_mem_nhds_iff — Mathlib

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]

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