compl_singleton_mem_nhdsSet_iff — Mathlib

English

In a T1 space, for any x ∈ X and any set s ⊆ X, the complement {x}^c belongs to the neighborhood-set filter of s if and only if x ∉ s.

Русский

В T1-пространстве для любого x и множества s комплемент {x} принадлежит фильтру окрестностей множества s тогда и только тогда, когда x не принадлежит s.

LaTeX

$$$\{x\}^c \in \mathcal{N}_{\mathrm{nhds}}(s) \;\;\iff \;\; x \notin s$$$

Lean4

@[simp]
theorem compl_singleton_mem_nhdsSet_iff [T1Space X] {x : X} {s : Set X} : { x }ᶜ ∈ 𝓝ˢ s ↔ x ∉ s := by
  rw [isOpen_compl_singleton.mem_nhdsSet, subset_compl_singleton_iff]

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