Iio_mem_nhds — Mathlib

English

Let a and b be elements with a < b in a linearly ordered topological space; then the open ray (−∞, b) is a neighborhood of a.

Русский

Пусть a и b — элементы линейно упорядоченного топологического пространства и a < b. Тогда луч (−∞, b) является окрестностью точки a.

LaTeX

$$$a < b \rightarrow (-\infty, b) \in 𝓝 a$$$

Lean4

theorem Iio_mem_nhds (h : a < b) : Iio b ∈ 𝓝 a :=
  isOpen_Iio.mem_nhds h

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