# 鄰域

集合 N 是點 x 的鄰域，當且僅當 N 包含某個含 x 的開集；N 本身不必開。

mko-neighborhood · definition · v0.10.0



## 數學敘述

在拓撲空間 (X,τ) 中，N⊆X 是 x∈X 的鄰域，當且僅當存在 U∈τ，使 x∈U⊆N。所有含 x 的開集構成 x 的開鄰域基礎，但一般鄰域本身不必開。





## 代表公式（精確 TeX）

x\in N





## 成立條件


- X、τ、x 與候選 N 已明示，且 x∈X、N⊆X。
- 鄰域採包含開集的集合語義；不預設距離、半徑或單一最小鄰域。





## 符號作用域


- x — 指定點
- N — 候選鄰域





## 直觀、定義與常見誤解

核對 N 是否為鄰域時，應搜尋所有含 x 且包含於 N 的開集見證。N 自己不是開集也可能是鄰域。

鄰域具有向上封閉性：若 N 是 x 的鄰域且 N⊆M⊆X，則 M 也是 x 的鄰域。

有限拓撲可完整列出某點的全部鄰域；這個列表依賴拓撲與點，不能只看底集合。

把鄰域等同於開集或開球，或只檢查 x∈N 就宣稱 N 是鄰域。





## 已採用的推導導讀

[鄰域：在四點拓撲中搜尋開集見證並列出全部鄰域](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-neighborhood-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [拓撲空間](https://ocme.evemisslab.com/zh-Hant/mko/mko-topological-space/) — 鄰域由開集族導出。
- [開集與閉集](https://ocme.evemisslab.com/zh-Hant/mko/mko-open-closed-set/) — 見證 U 必須是開集。
- [集合隸屬](https://ocme.evemisslab.com/zh-Hant/mko/mko-set-membership/) — 指定點需屬於開集見證與候選鄰域。





## 驗證界線

有限冪集枚舉可完整核對指定模型；不外推度量球或一般濾子定理。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

綁定 nhds、nhds_basis_opens 與 neighborhood filter 的向上封閉語義。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/neighborhood.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-neighborhood/index.md)