nhdsWithin_neBot_of_mem

Mathlib.Topology.ContinuousOn

URI: https://scilib.ai/kg/mathlib#nhdsWithin_neBot_of_mem

English

If x ∈ s, then nhdsWithin x s is nonempty.

Русский

Если x принадлежит s, то nhdsWithin x s не пусто.

LaTeX

$$$$ x \\in s \\Rightarrow (\\\\nhdsWithin x s).NeBot. $$$$

Lean4

theorem nhdsWithin_neBot_of_mem {s : Set α} {x : α} (hx : x ∈ s) : NeBot (𝓝[s] x) :=
  mem_closure_iff_nhdsWithin_neBot.1 <| subset_closure hx

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

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

Разделы

Аффилиация

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