compl_mem_nhds

Mathlib.Topology.Neighborhoods

URI: https://scilib.ai/kg/mathlib#IsClosed.compl_mem_nhds

English

If s is closed and x ∉ s, then the complement sᶜ is a neighborhood of x.

Русский

Если s замкнутое множество и x не принадлежит s, то его комплемент sᶜ является окрестностью x.

LaTeX

$$$ s^c \in \mathcal N(x). $$$

Lean4

theorem compl_mem_nhds (hs : IsClosed s) (hx : x ∉ s) : sᶜ ∈ 𝓝 x :=
  hs.isOpen_compl.mem_nhds (mem_compl hx)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru