Iic_mem_nhds — Mathlib

English

If a < b in a linearly ordered space, then the closed lower ray (−∞, b] is a neighborhood of a.

Русский

Пусть a < b в линейно упорядоченном пространстве; тогда нижняя закрытая полупрямая (−∞, b] является окрестностью точки a.

LaTeX

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

Lean4

theorem Iic_mem_nhds (h : a < b) : Iic b ∈ 𝓝 a :=
  mem_of_superset (Iio_mem_nhds h) Iio_subset_Iic_self

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