nhds_true — Mathlib

English

The neighborhood filter of True equals the pure filter at True in the Sierpinski space.

Русский

Фильтр окрестностей True равен чистому фильтру True в терминах пространства Сирпенски.

LaTeX

$$$\\mathcal{N}(\\text{True}) = \\text{pure}({\\text{True}}).$$$

Lean4

@[simp]
theorem nhds_true : 𝓝 True = pure True :=
  le_antisymm (le_pure_iff.2 <| isOpen_singleton_true.mem_nhds <| mem_singleton _) (pure_le_nhds _)

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