# 緊緻把分離鄰域縮為有限個 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-compact-subset-closed-in-hausdorff/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-compact-subset-closed-in-hausdorff-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 證 Hausdorff 空間中的緊緻子集 K 閉。 給出覆蓋的一般論證；有限例子不取代此證明，且不證逆命題。 ## 已知條件與符號 - sets - topology - hausdorff_def - compact_def - G1 — X 是 Hausdorff，K 以子空間拓撲緊緻。 - U_y,V_y — 分離鄰域 - m — 有限子覆蓋大小 ## 規則與來源 - mko_definition · cited — 對每個x∉K及每個y∈K，以Hausdorff性選不交open neighborhoods U_y含x與V_y含y；{V_y}覆蓋K，compactness給有限subcover。相應有限個U_y的交集是與K不交的open neighborhood of x，故X\K open。empty compact subset亦closed。Hausdorff假設不可刪；converse也不成立。 · mko-compact-subset-closed-in-hausdorff - sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。 - topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。 - hausdorff_def · prerequisite — Hausdorff：每對異點各有不交開鄰域包含指定點。 - compact_def · prerequisite — K 緊緻表示每個相對開覆蓋有有限原索引子覆蓋；相對開集為母開集與 K 之交。 ## 逐步主鏈 S01 · case_split操作前 K=\varnothing 操作後 X\setminus K=X\text{ is open} 條件：無 規則：sets · 依賴：G1 葉節點依據：sets 先處理空 K，空集閉直接來自全集開。 S02 · implies操作前 K\ne\varnothing,\quad x\in X\setminus K 操作後 x\ne y\quad\forall y\in K 條件：K\ne\varnothing 規則：sets · 依賴：G1 葉節點依據：sets 以下固定任意外點 x；因它不在 K，所以不同於每個 y。 S03 · theorem_application操作前 x\ne y\in K\cup\{x\} 操作後 x\in U_y,\ y\in V_y,\ U_y,V_y\text{ open},\ U_y\cap V_y=\varnothing 條件：無 規則：hausdorff_def · 依賴：G1, S02, hausdorff_def 葉節點依據：hausdorff_def 逐 y 使用 Hausdorff 分離，兩側鄰域同時保留。 S04 · implies操作前 y\in K\cap V_y\quad(y\in K) 操作後 K\subseteq\bigcup_{y\in K}(K\cap V_y) 條件：無 規則：sets · 依賴：S03 葉節點依據：sets 每個 y 被自己的 V_y 覆蓋，且相交 K 為相對開。 S05 · theorem_application操作前 (K\cap V_y)_{y\in K}\text{ covers }K 操作後 K\subseteq\bigcup_{j=1}^{m}V_{y_j},\quad m\in\mathbb N 條件：K\ne\varnothing 規則：compact_def · 依賴：G1, S04, compact_def 葉節點依據：compact_def 緊緻性選有限多個原索引；因 K 非空可以取 m≥1。 S06 · implies操作前 U=\bigcap_{j=1}^{m}U_{y_j} 操作後 U\text{ is open and }x\in U 條件：m<\infty 規則：topology · 依賴：S03, S05 葉節點依據：topology 有限交保開，每項含 x，故交仍含 x。 S07 · implies操作前 z\in U\cap K 操作後 z\in V_{y_j}\cap U_{y_j}=\varnothing\text{ for some }j 條件：無 規則：sets · 依賴：S03, S05, S06 葉節點依據：sets 若有 z 同在 U 與 K，有限子覆蓋選到含 z 的 V；U 又包含於對應 U，矛盾。 S08 · implies操作前 \forall x\in X\setminus K\ \exists U_x\text{ open}:x\in U_x\subseteq X\setminus K 操作後 X\setminus K=\bigcup_{x\notin K}U_x\text{ open};\quad K\text{ closed} 條件：無 規則：topology · 依賴：S01, S02, S06, S07 葉節點依據：topology 補集是這些開鄰域的聯，所以開；若補集空，空聯也開。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · S01, S02, S06, S07 — 只得到正向定理，沒有反轉成閉集皆緊緻。 - S07 · premise_audit · S03, S05, S06 — 每個 z 可用不同 j；不需一個 V 覆蓋整個 K。 - S06 · premise_audit · S03, S05 — 使用有限而非任意交公理。 - S05 · premise_audit · G1, S04, compact_def — 有限性是下一步開交成立的必要橋梁。 - S04 · premise_audit · S03 — 不是主張所有 U_y 交集已開；那可能是無限交。 - S03 · premise_audit · G1, S02, hausdorff_def — 只核一個 y 的鄰域不能覆蓋整個 K。 - S02 · premise_audit · G1 — x 的任意性會在最後給整個補集開。 - S01 · premise_audit · G1 — 此分支不需選 K 內的點或非空子覆蓋。 ## 錯誤控制與反例 有限交橋梁先選有限 V 子覆蓋，才交對應 U。 點對量詞對固定外點與每個 K 內點分離，最後再放開外點。 - 任意拓撲空間的緊緻子集都閉。 → reject — 在只以空集、全集為開集的兩點空間中，單點集緊緻但不閉。 - 所有 U_y 的無限交必開。 → reject — 拓撲只保有限交開，需先用緊緻性。 - 實數線的所有閉集都緊緻。 → reject — R 閉；覆蓋 (-n,n), n≥1 沒有有限子覆蓋。 ## 結論與限制 在所列兩項假設下 K 閉，空 K 亦包含。 ## 驗證及來源綁定 0 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 813fe0a58f2f6c26c88fc29c4ab65d01c638ff0c78dbb769f371543294dd6ab7 - original source SHA-256: 70031bac985789aa1c49e84f0a64049275096117bd97bc22051b96b5a3ce3cac - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-compact-subset-closed-in-hausdorff-01.json)