mem_nhds_iff

Mathlib.Topology.Neighborhoods

URI: https://scilib.ai/kg/mathlib#IsOpen.mem_nhds_iff

English

Given a closed set s and a point x not in s, the complement s^c is a neighborhood of x.

Русский

Если s замкнуто и x ∉ s, то комплемент s^c является окрестностью x.

LaTeX

$$$s^c \\in \\mathcal{N}(x)$, если s замкнуто и x ∉ s$$

Lean4

protected theorem mem_nhds_iff (hs : IsOpen s) : s ∈ 𝓝 x ↔ x ∈ s :=
  ⟨mem_of_mem_nhds, fun hx => mem_nhds_iff.2 ⟨s, Subset.rfl, hs, hx⟩⟩

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

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

Разделы

Аффилиация

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