緊緻把分離鄰域縮為有限個

目標與範圍

證 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 之交。

逐步主鏈

K=\varnothing

X\setminus K=X\text{ is open}

K\ne\varnothing,\quad x\in X\setminus K

x\ne y\quad\forall y\in K

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

y\in K\cap V_y\quad(y\in K)

K\subseteq\bigcup_{y\in K}(K\cap V_y)

(K\cap V_y)_{y\in K}\text{ covers }K

K\subseteq\bigcup_{j=1}^{m}V_{y_j},\quad m\in\mathbb N

U=\bigcap_{j=1}^{m}U_{y_j}

U\text{ is open and }x\in U

z\in U\cap K

z\in V_{y_j}\cap U_{y_j}=\varnothing\text{ for some }j

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

局部子步與引理

本稿無局部子步。

逐步反向審查

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