mem_of_nhdsWithin_neBot

Mathlib.Topology.ContinuousOn

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

← MathLib Explorer

English

If s is closed and nhdsWithin_neBot at x, then x ∈ s.

Русский

Если s замкнуто и nhdsWithin(x) не пусто, то x ∈ s.

LaTeX

$$$$ \\text{IsClosed}(s) \\; \\wedge\\; (\\\\nhdsWithin x s).NeBot \\Rightarrow x \\in s. $$$$

Lean4

theorem mem_of_nhdsWithin_neBot {s : Set α} (hs : IsClosed s) {x : α} (hx : NeBot <| 𝓝[s] x) : x ∈ s :=
  hs.closure_eq ▸ mem_closure_iff_nhdsWithin_neBot.2 hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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