# 鄰域：在四點拓撲中搜尋開集見證並列出全部鄰域

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-neighborhood/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-neighborhood-01 · production-20261019-adopted-96



## 目標與範圍

設 X={1,2,3,4}，τ={∅,{1},{1,2},{3,4},{1,3,4},X}。判定 N1={1,2,3} 與 N2={2,3,4} 是否為點 2 的鄰域；證明在有限拓撲中，點 x 的鄰域恰是包含 O_x（含 x 的全部開集之交）的子集，據此列出點 1、2、3、4 的全部鄰域；證明鄰域向上封閉；並說明同一集合在離散拓撲下的判定可能不同。

在 MKO 範圍內工作：X、τ、點與候選集合都明示（假設 a1），鄰域採「包含一個含該點的開集」的語義，不用距離或半徑，也不預設最小鄰域（假設 a2）；本例的最小鄰域 O_x 是由 τ 有限推出，不是假設。不處理鄰域濾子的形式化，不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- subset_def
- set_operations_def
- finite_counting_basics
- nat_induction


- G1 — 底集合 X={1,2,3,4}，拓撲 τ={∅,{1},{1,2},{3,4},{1,3,4},X}（MKO 假設 a1）。
- G2 — 候選點與集合：x=2，N1={1,2,3}，N2={2,3,4}；都滿足 x∈X 與 N⊆X。
- G3 — 比較用的離散拓撲 δ=P(X)，即 X 的每個子集都是開集。


- X — 底集合 {1,2,3,4}
- \tau — X 上的拓撲
- \tau_x — 含 x 的開集族 {U∈τ ∣ x∈U}
- O_x — τ_x 全部成員之交
- \mathcal{N}(x) — x 的全部鄰域
- \delta — X 上的離散拓撲 P(X)





## 規則與來源


- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- topology_def · prerequisite — 拓撲：X 上的開集族 τ 包含 ∅ 與 X，對任意聯集與有限交集封閉。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- mko_neighborhood_def · cited — 在拓撲空間 (X,τ) 中，N⊆X 是 x∈X 的鄰域，當且僅當存在 U∈τ，使 x∈U⊆N。所有含 x 的開集構成 x 的開鄰域基礎，但一般鄰域本身不必開。 · mko-neighborhood
- mko_topological_space_def · cited — X 上的拓撲是子集合族 τ⊆P(X)，滿足 ∅∈τ、X∈τ、任意子族的聯集在 τ、任意有限子族的交集在 τ（空族交集按 X 解讀）。 · mko-topological-space
- finite_witness_search · prerequisite — 對明示列出的有限集合 F，∃U∈F, Q(U) 等價於 Q 對某個列出成員成立；要否定它，必須逐一檢查 F 的每個成員都不滿足 Q。
- L_least_open · lemma — 設 (X,τ) 是拓撲空間且 τ 有限，x∈X，O_x=∩{U∈τ ∣ x∈U}。則 O_x∈τ、x∈O_x，且對每個 N⊆X：N 是 x 的鄰域當且僅當 O_x⊆N。
- L_upward · lemma — 在任何拓撲空間中，若 N 是 x 的鄰域且 N⊆M⊆X，則 M 也是 x 的鄰域。





## 逐步主鏈

S01 · implies操作前

\tau=\{\varnothing,\{1\},\{1,2\},\{3,4\},\{1,3,4\},X\}

操作後

(X,\tau)\ \text{is a topological space}

條件：\tau\ \text{finite}

規則：topology_def · 依賴：G1

葉節點依據：topology_def + set_operations_def + nat_induction

確認前提：六個成員都是 X 的子集，∅、X∈τ。四個非平凡成員兩兩的聯集與交集為：{1}、{1,2} 得 {1,2} 與 {1}；{1}、{3,4} 得 {1,3,4} 與 ∅；{1}、{1,3,4} 得 {1,3,4} 與 {1}；{1,2}、{3,4} 得 X 與 ∅；{1,2}、{1,3,4} 得 X 與 {1}；{3,4}、{1,3,4} 得 {1,3,4} 與 {3,4}，全在 τ 中。τ 有限，每個子族都有限，對成員數歸納即由兩兩封閉與 ∅、X∈τ 得到任意子族的聯集與有限交集封閉。



S02 · equivalent操作前

N\in\mathcal{N}(x)

操作後

\exists U\in\tau,\ x\in U\ \wedge\ U\subseteq N

條件：x\in X,\ N\subseteq X

規則：def_unfold · 依賴：S01, mko_neighborhood_def

葉節點依據：def_unfold + mko_neighborhood_def

展開 MKO 定義：N 是 x 的鄰域，當且僅當有一個開集見證 U 同時含 x 且包含於 N。τ 只有六個成員，所以存在量詞的搜尋範圍是有限的：肯定時只需給出一個見證，否定時必須排除所有六個成員（finite_witness_search）。



S03 · implies操作前

\tau_2=\{U\in\tau\mid 2\in U\}

操作後

\tau_2=\{\{1,2\},X\}

條件：無

規則：set_builder · 依賴：G1

葉節點依據：set_builder + finite_witness_search

逐一檢查 τ 的成員是否含 2：∅ 否、{1} 否、{1,2} 是、{3,4} 否、{1,3,4} 否、X 是。所以點 2 的候選見證只有 {1,2} 與 X。



S04 · implies操作前

N_1=\{1,2,3\}

操作後

U=\{1,2\}:\ 2\in U,\ U\subseteq N_1\ \Rightarrow\ N_1\in\mathcal{N}(2)

條件：無

規則：exists_intro · 依賴：S02, S03, G2

葉節點依據：exists_intro + subset_def

取見證 U={1,2}∈τ：2∈U，且 U 的元素 1、2 都在 N1 中，所以 U⊆N1。依 S02 與 ∃引入，N1 是 2 的鄰域。



S05 · implies操作前

N_1=\{1,2,3\}

操作後

N_1\notin\tau

條件：無

規則：finite_witness_search · 依賴：G1, G2

葉節點依據：finite_witness_search + set_extensionality

把 N1 與 τ 的六個成員逐一比較，沒有一個等於 {1,2,3}，所以 N1 不是開集。與 S04 合起來：N1 是 2 的鄰域，卻不是開集。鄰域不必是開集。



S06 · implies操作前

N_2=\{2,3,4\},\ 2\in N_2

操作後

\{1,2\}\not\subseteq N_2,\ X\not\subseteq N_2\ \Rightarrow\ N_2\notin\mathcal{N}(2)

條件：無

規則：quantifier_negation · 依賴：S02, S03, G2

葉節點依據：quantifier_negation + finite_witness_search + subset_def

雖然 2∈N2，仍需找見證。依 S03，只有 {1,2} 與 X 含 2；兩者都含 1，而 1∉N2，所以都不包含於 N2。其餘四個開集不含 2，不能當見證。沒有見證，依量詞否定，N2 不是 2 的鄰域。



S07 · theorem_application操作前

O_x=\textstyle\bigcap\{U\in\tau\mid x\in U\}

操作後

O_x\in\tau,\ x\in O_x,\ (N\in\mathcal{N}(x)\iff O_x\subseteq N)

條件：\tau\ \text{finite}

規則：L_least_open · 依賴：S01

葉節點依據：topology_def + set_operations_def + subset_def

為了列出全部鄰域，套用引理 L_least_open（在 S07.1 到 S07.3 證明）：τ 有限時，含 x 的全部開集之交 O_x 本身是開集且含 x，而且 N 是 x 的鄰域恰好當 O_x⊆N。於是「搜尋見證」化為「檢查一個包含關係」。這個最小開鄰域是由有限性推出的，不是 MKO 假設 a2 所禁止的預設。



S08 · implies操作前

O_2=\{1,2\}\cap X

操作後

O_2=\{1,2\},\ \mathcal{N}(2)=\{\{1,2\},\{1,2,3\},\{1,2,4\},X\}

條件：無

規則：L_least_open · 依賴：S03, S07

葉節點依據：L_least_open + finite_counting_basics

由 S03，O_2={1,2}∩X={1,2}。依 S07，2 的鄰域恰是包含 {1,2} 的子集；元素 3、4 可自由選擇是否加入，共 2^2=4 個：{1,2}、{1,2,3}、{1,2,4}、X。這與 S04（N1 含 {1,2}）和 S06（N2 不含 1）一致。



S09 · implies操作前

\tau_1=\{\{1\},\{1,2\},\{1,3,4\},X\}

操作後

O_1=\{1\},\ \mathcal{N}(1)=\{N\subseteq X\mid 1\in N\}

條件：無

規則：L_least_open · 依賴：G1, S07

葉節點依據：L_least_open + set_builder + finite_counting_basics

含 1 的開集是 {1}、{1,2}、{1,3,4}、X，交集 O_1={1}。所以 1 的鄰域恰是所有含 1 的子集，2、3、4 各自可選，共 2^3=8 個。點 1 的鄰域比點 2 多，因為 {1} 本身是開集。



S10 · implies操作前

\tau_3=\tau_4=\{\{3,4\},\{1,3,4\},X\}

操作後

O_3=O_4=\{3,4\},\ \mathcal{N}(3)=\mathcal{N}(4)=\{\{3,4\},\{1,3,4\},\{2,3,4\},X\}

條件：無

規則：L_least_open · 依賴：G1, S07

葉節點依據：L_least_open + set_builder

含 3 的開集與含 4 的開集是同一族：{3,4}、{1,3,4}、X，交集都是 {3,4}。所以 3 與 4 的鄰域完全相同，共 4 個。注意 N2={2,3,4} 是 3 與 4 的鄰域，卻不是 2 的鄰域（S06）：同一集合是否為鄰域取決於點。



S11 · theorem_application操作前

N\in\mathcal{N}(x),\ N\subseteq M\subseteq X

操作後

M\in\mathcal{N}(x)

條件：N\subseteq M\subseteq X

規則：L_upward · 依賴：S04

葉節點依據：subset_def + mko_neighborhood_def

套用向上封閉引理 L_upward（在 S11.1 證明，適用於任何拓撲空間）。例：N1={1,2,3} 是 2 的鄰域且 N1⊆X，所以 X 也是 2 的鄰域，與 S08 的列表一致。



S12 · implies操作前

\{2\}\ \text{under}\ \tau\ \text{and under}\ \delta

操作後

\{2\}\notin\mathcal{N}_\tau(2),\quad \{2\}\in\mathcal{N}_\delta(2)

條件：無

規則：mko_neighborhood_def · 依賴：G3, S08

葉節點依據：mko_neighborhood_def + exists_intro + quantifier_negation

在 τ 下，O_2={1,2}⊄{2}，所以 {2} 不是 2 的鄰域（S08）。在離散拓撲 δ 下，{2}∈δ 本身就是含 2 的開集，自己就是見證，所以 {2} 是 2 的鄰域。同一個底集合、同一個點、同一個候選集合，換了拓撲判定就改變：鄰域列表依賴拓撲與點，不能只看底集合（MKO 第三段）。







## 局部子步與引理

S07.1 · implies操作前

\tau_x=\{U\in\tau\mid x\in U\}

操作後

O_x\in\tau,\ x\in O_x

條件：\tau\ \text{finite}

規則：mko_topological_space_def · 依賴：mko_topological_space_def, set_operations_def

葉節點依據：mko_topological_space_def + set_operations_def

τ_x 是 τ 的子族，因 τ 有限而有限；又 X∈τ_x，所以非空。依拓撲公理，有限子族的交集在 τ 中，故 O_x∈τ。τ_x 的每個成員都含 x，所以 x 在它們的交集中。



S07.2 · implies操作前

O_x\subseteq N

操作後

N\in\mathcal{N}(x)

條件：無

規則：exists_intro · 依賴：S07.1, mko_neighborhood_def

葉節點依據：exists_intro + mko_neighborhood_def

(⇐) 若 O_x⊆N，取見證 U=O_x：由 S07.1，U∈τ 且 x∈U，又 U⊆N，所以 N 是 x 的鄰域。



S07.3 · implies操作前

N\in\mathcal{N}(x)

操作後

O_x\subseteq N

條件：無

規則：exists_elim · 依賴：S07.1, mko_neighborhood_def

葉節點依據：exists_elim + set_operations_def + subset_def

(⇒) 若 N 是 x 的鄰域，取其見證 U：U∈τ、x∈U、U⊆N。則 U∈τ_x，交集 O_x 包含於每個成員，故 O_x⊆U⊆N。S07.1 到 S07.3 合起來證得 L_least_open。



S11.1 · implies操作前

x\in U\subseteq N\subseteq M,\ U\in\tau

操作後

x\in U\subseteq M\ \Rightarrow\ M\in\mathcal{N}(x)

條件：無

規則：subset_def · 依賴：mko_neighborhood_def, subset_def

葉節點依據：subset_def + mko_neighborhood_def + forall_intro

設 U 是 N 的見證。由 U⊆N 與 N⊆M，依 ⊆ 的傳遞得 U⊆M；U 仍是含 x 的開集，所以同一個 U 也是 M 的見證，M 是 x 的鄰域。x、N、M 都是任意的，證得 L_upward。







## 逐步反向審查


- S12 · premise_audit · G3, S08, mko_neighborhood_def — 兩個判定各自只用到對應拓撲的定義；不宣稱 δ 下的其他結論。
- S11.1 · premise_audit · mko_neighborhood_def, subset_def, forall_intro — 只用到定義與包含的傳遞，沒有用到 τ 有限，所以對任何拓撲空間成立。
- S11 · premise_audit · L_upward, S04 — 向上封閉不給出向下封閉：{1,2} 是 2 的鄰域，但其子集 {2} 不是。
- S10 · premise_audit · G1, S07 — τ_3 與 τ_4 都由逐一檢查六個成員得到（N5 記錄大小 3）。
- S09 · premise_audit · G1, S07, finite_counting_basics — τ_1 由逐一檢查六個成員得到（N4 記錄其大小 4）；計數見 N3。
- S08 · premise_audit · S03, S07, finite_counting_basics — 列表完整性來自引理的雙向等價與子集計數（N2）。
- S07.3 · premise_audit · S07.1, exists_elim, subset_def — 用到交集包含於每個成員與 ⊆ 的傳遞；結論不提及見證 U，符合 ∃消去的條件。
- S07.2 · premise_audit · S07.1, mko_neighborhood_def, exists_intro — 見證 O_x 必須是開集，這正是 S07.1 的結論。
- S07.1 · premise_audit · mko_topological_space_def, set_operations_def — 關鍵是有限交集公理；若 τ_x 無限，交集不一定開。
- S07 · premise_audit · L_least_open, S01 — 引理需要 τ 有限；在 ℝ 的通常拓撲中，含 0 的開集之交是 {0}，不是開集，0 沒有最小鄰域（見錯誤控制三）。
- S06 · premise_audit · S03, quantifier_negation, finite_witness_search — 否定存在命題必須排除全部六個成員：四個因不含 2 排除，兩個因不包含於 N2 排除。
- S05 · premise_audit · G1, finite_witness_search — 「不是開集」需要比較全部六個成員。
- S04 · premise_audit · S02, S03, exists_intro, subset_def — 一個見證就足夠；見證必須是 τ 的成員，不能用任意含 2 的集合。
- S03 · premise_audit · G1, set_builder, finite_witness_search — 六個成員全部檢查過，所以 τ_2 的列表完整（N1 記錄其大小 2）。
- S02 · inverse_equivalence · mko_neighborhood_def, def_unfold — 展開與折回定義互為反向。注意條件是兩個：x∈U 與 U⊆N，只有 x∈N 不夠。
- S01 · premise_audit · G1, topology_def, mko_topological_space_def, nat_induction — 需要完整的兩兩檢查與 τ 有限；若 τ 不是拓撲，鄰域的定義就沒有意義。





## 錯誤控制與反例

鄰域不必是開集MKO 指出的誤解是把鄰域等同於開集或開球。N1={1,2,3} 不在 τ 中，卻因為包含開集 {1,2}∋2 而是 2 的鄰域（S04、S05）。鄰域的定義只要求「包含」一個含點的開集。

只檢查 x∈N 不夠N2={2,3,4} 含 2，但含 2 的開集 {1,2} 與 X 都含 1，無法放進 N2（S06）。判定鄰域必須搜尋開集見證，否定時要排除所有候選。

最小鄰域來自有限性，不是一般事實S07 的 O_x 之所以開，是因為 τ 有限，交集是有限交。在 ℝ 的通常拓撲中，若 N 是 0 的最小鄰域，它要包含於每個以正整數 n≥1 編號的區間 (−1/n,1/n)，依阿基米德性質 N⊆{0}，即 N={0}；但 {0} 不包含任何含 0 的開區間，不是 0 的鄰域，矛盾。所以 0 沒有最小鄰域，不能把本例的做法推廣成一般假設（MKO 假設 a2）。


- {1,2,3} 不是開集，所以它不是點 2 的鄰域 → reject — 見證 {1,2}∈τ 滿足 2∈{1,2}⊆{1,2,3}。
- 2∈{2,3,4}，所以 {2,3,4} 是點 2 的鄰域 → reject — 含 2 的開集只有 {1,2} 與 X，兩者都含 1∉{2,3,4}，沒有見證。
- 單點集 {2} 一定是點 2 的鄰域 → reject — 在 τ 下 O_2={1,2}⊄{2}；只有在像離散拓撲這樣 {2} 為開集的拓撲中才成立。
- 3 與 4 是不同的點，所以它們的鄰域族一定不同 → reject — O_3=O_4={3,4}，兩點的鄰域族完全相同（S10）。





## 結論與限制

N1={1,2,3} 是點 2 的鄰域（見證 {1,2}）但不是開集；N2={2,3,4} 含 2 卻不是 2 的鄰域。在有限拓撲中 N 是 x 的鄰域當且僅當 O_x⊆N；本例 O_1={1}、O_2={1,2}、O_3=O_4={3,4}，所以 1 有 8 個鄰域，2 有 4 個，3 與 4 各有相同的 4 個。鄰域向上封閉；在離散拓撲下 {2} 是 2 的鄰域，在 τ 下則不是。


- 與 Mathlib 的 nhds、nhds_basis_opens 與鄰域濾子向上封閉語義的綁定（MKO formal next）未在此建立。





## 驗證及來源綁定

5 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: a79028f77322db110cfe9e06c126ca7f2fafe3f16ff676c8b59b56e6bad4389a
- original source SHA-256: b21c0ed8194f848c969d43585bab34a26ff70a3a4c37bb4e3de7b9931a5e0ef4
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-neighborhood-01.json)