nhds_eq_pure — Mathlib

English

The neighborhood filter equals the pure filter at a exactly when a is not a succ-limit.

Русский

Фильтр окрестностей равен чистому фильтру в точке a тогда и только тогда, когда a не succ-limit.

LaTeX

$$$\mathcal{N}(a) = \text{pure}(a) \iff \lnot \text{IsSuccLimit}(a)$$$

Lean4

theorem nhds_eq_pure : 𝓝 a = pure a ↔ ¬IsSuccLimit a :=
  (isOpen_singleton_iff_nhds_eq_pure _).symm.trans isOpen_singleton_iff

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