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

目標與範圍

設 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 的鄰域。

逐步主鏈

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

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

N\in\mathcal{N}(x)

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

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

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

N_1=\{1,2,3\}

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

N_1=\{1,2,3\}

N_1\notin\tau

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)

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)

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

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

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

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

\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\}

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

M\in\mathcal{N}(x)

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

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

局部子步與引理

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

O_x\in\tau,\ x\in O_x

O_x\subseteq N

N\in\mathcal{N}(x)

N\in\mathcal{N}(x)

O_x\subseteq N

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

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

逐步反向審查

• 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、反控制與修訂記錄）