mem_closure_iff_nhdsWithin_neBot

Mathlib.Topology.ClusterPt

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

English

x ∈ closure s iff nhds x restricted to s is nontrivial.

Русский

x принадлежит замыканию s тогда и только тогда, когда nhds x, ограниченный до s, не тривиален.

LaTeX

$$$x \in \overline{s} \iff \mathrm{NHDS}_x|_s \neq \bot$$$

Lean4

theorem mem_closure_iff_nhdsWithin_neBot : x ∈ closure s ↔ NeBot (𝓝[s] x) :=
  mem_closure_iff_clusterPt

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

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

Разделы

Аффилиация

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