isOpen_singleton_iff_nhds_eq_pure

English

For any x, the singleton {x} is open iff the neighborhood filter at x equals the pure filter at x.

Русский

Для любой точки x множество {x} открыто тогда и только тогда, когда 𝓝(x) = pure(x).

LaTeX

$$$\\text{IsOpen}(\{x\\}) \\iff 𝓝(x) = \\mathrm{pure}(x)$$$

Lean4

theorem isOpen_singleton_iff_nhds_eq_pure (x : X) : IsOpen ({ x } : Set X) ↔ 𝓝 x = pure x := by
  simp [← (pure_le_nhds _).ge_iff_eq', isOpen_iff_mem_nhds]

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