mem_nhds

Mathlib.Topology.Neighborhoods

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

English

For an open set s in a topological space, s ∈ 𝓝 x if and only if x ∈ s.

Русский

Для открытого множества s в топологическом пространстве выполняется: s ∈ 𝓝 x ⇔ x ∈ s.

LaTeX

$$$s \\in \\mathcal{N}(x) \\iff x \\in s$ (для открытого s)$$

Lean4

theorem mem_nhds (hs : IsOpen s) (hx : x ∈ s) : s ∈ 𝓝 x :=
  mem_nhds_iff.2 ⟨s, Subset.refl _, hs, hx⟩

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

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

Разделы

Аффилиация

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