Ioc_mem_nhds_iff — Mathlib

English

In a densely ordered, order-topological space with no maximum, a set Ioc(a,b) is a neighborhood of x exactly when x lies strictly between a and b.

Русский

В плотно упорядоченном пространстве с порядковой топологией и без максимального элемента, Ioc(a,b) является окрестностью x тогда и только тогда, когда x находится внутри (a,b).

LaTeX

$$$Ioc(a,b) \in \mathcal{N}(x) \iff x \in Ioo(a,b)$$$

Lean4

@[simp]
theorem Ioc_mem_nhds_iff [NoMaxOrder α] {a b x : α} : Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b := by
  rw [← interior_Ioc, mem_interior_iff_mem_nhds]

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