nhds_discrete — Mathlib

English

In a discrete topological space, the neighborhood filter at every point x coincides with the principal filter at x, i.e., nhds x = pure x.

Русский

В дискретном пространстве фильтр окрестностей в точке x совпадает с главной фильтром в x, то есть nhds x = pure x.

LaTeX

$$$\forall x,\ nhds(x) = \mathrm{pure}(x)$$$

Lean4

@[simp]
theorem nhds_discrete (α : Type*) [TopologicalSpace α] [DiscreteTopology α] : @nhds α _ = pure :=
  le_antisymm (fun _ s hs => (isOpen_discrete s).mem_nhds hs) pure_le_nhds

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