notMem_closure_iff_nhdsWithin_eq_bot

Mathlib.Topology.ClusterPt

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

English

x ∉ closure s iff nhdsWithin x (s \ {x}) = ⊥

Русский

x не принадлежит замыканию s тогда и только тогда, когда nhdsWithin x (s \ {x}) = ⊥

LaTeX

$$$x \notin \overline{s} \iff \mathcal{N}_{x}^{s \setminus \{x\}} = \bot$$$

Lean4

theorem notMem_closure_iff_nhdsWithin_eq_bot : x ∉ closure s ↔ 𝓝[s] x = ⊥ := by
  rw [mem_closure_iff_nhdsWithin_neBot, not_neBot]

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

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

Разделы

Аффилиация

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