# 正规空间的邻域里有闭邻域　`prop.normal-locally-closed`
命题：正规 Hausdorff $\implies$ 每个邻域含闭邻域
layer 7 · 命题 · 拓扑空间 · 拓扑学
[在星图里打开](../#n=prop.normal-locally-closed)　·　[节点索引](../index.md)

设 $X$ 是**正规** Hausdorff 空间、$x \in X$。则 $x$ 的每个邻域都含一个**闭**邻域。

## 为什么成立（入边，证明在 proofs/）
- [`def.normal-space`](../nodes/def.normal-space.md) 正规空间：用到了定义 正规空间　[proofs/def-link.normclosed-normal.md](../proofs/def-link.normclosed-normal.md)

refs: Le Stum, An introduction to condensed mathematics, Exercise 2.5

> 说明见 `notes/prop.normal-locally-closed.md`

引用：`prop.normal-locally-closed`（内容 v0.9.0）· 条款见 [LICENSE.txt](../LICENSE.txt)