mem_nhds_discrete

Mathlib.Topology.Order

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

English

For a discrete space, a set s is a neighborhood of x exactly when x ∈ s.

Русский

Для дискретного пространства множество s является окрестностью точки x тогда и только тогда, когда x ∈ s.

LaTeX

$$$s \in \mathcal{N H D S}(x) \iff x \in s$$$

Lean4

theorem mem_nhds_discrete {x : α} {s : Set α} : s ∈ 𝓝 x ↔ x ∈ s := by rw [nhds_discrete, mem_pure]

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

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

Разделы

Аффилиация

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