# 有限子空間的緊緻性

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

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

derivation-mko-compact-subset-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

證 K={b,c} 在指定母空間中緊緻，並核相對開覆蓋。

完整有限模型；不把緊緻普遍改寫成閉且有界。





## 已知條件與符號


- sets
- topology
- definition_here


- G1 — X={a,b,c}, tau={空集,{a},{a,b},X}, K={b,c}。


- \tau_K — 誘導拓撲
- V_i — 相對開覆蓋成員





## 規則與來源


- mko_definition · cited — cover須覆蓋K，subcover只能從original cover選取。單一cover通過不證一般compactness；完整有限topology/finite subset由有限性定理compact，空集採compact convention，但不得外推infinite spaces或把compact普遍當closed-and-bounded。 · mko-compact-subset
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。
- definition_here · prerequisite — K 的相對開集為 U∩K（U 母開）；K 緊緻指每個相對開覆蓋有取自原索引的有限子覆蓋。





## 逐步主鏈

S01 · implies操作前

\varnothing\subset\{a\}\subset\{a,b\}\subset X

操作後

\tau\text{ is a topology}

條件：無

規則：topology · 依賴：G1

葉節點依據：topology

含兩端的有限鏈對聯交封閉。



S02 · definition操作前

U\cap K\ (U\in\tau)

操作後

\varnothing,\varnothing,\{b\},K

條件：無

規則：definition_here · 依賴：G1, S01

葉節點依據：definition_here

逐個母開集相交，保留全部四項來源。



S03 · implies操作前

\tau_K=\{\varnothing,\{b\},K\}

操作後

\tau_K\text{ is a topology on }K

條件：無

規則：topology · 依賴：S02

葉節點依據：topology

去重後仍是含空集與 K 的有限鏈。



S04 · implies操作前

K\subseteq\bigcup_{i\in I}V_i,\quad V_i\in\tau_K

操作後

c\in V_j\text{ for some }j\in I

條件：無

規則：sets · 依賴：S03

葉節點依據：sets

任取相對開覆蓋，c 必落在某一原成員中。



S05 · implies操作前

c\in V_j\in\tau_K

操作後

V_j=K

條件：無

規則：sets · 依賴：S03, S04

葉節點依據：sets

完整相對族只有 K 含 c。



S06 · definition操作前

J=\{j\}\subseteq I,\quad\bigcup_{i\in J}V_i=K

操作後

K\text{ is compact in the subspace topology}

條件：無

規則：definition_here · 依賴：S04, S05

葉節點依據：definition_here

每個相對開覆蓋都有一項原成員子覆蓋，完成全稱定義。



S07 · implies操作前

(V_1,V_2)=(\{b\},K)

操作後

J=\{2\}\text{ covers }K;\quad\{1\}\text{ does not}

條件：無

規則：sets · 依賴：G1, S03

葉節點依據：sets

指定覆蓋也可回讀原索引；單取 {b} 漏 c。



S08 · implies操作前

K=\varnothing\text{ as a separate boundary}

操作後

\varnothing\text{ has the empty finite subcover}

條件：無

規則：sets · 依賴：S03

葉節點依據：sets

空子集同樣緊緻，不需從空覆蓋中捏造一個成員。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S03 — 空目標的聯集包含責任真，與非空例子不同。
- S07 · premise_audit · G1, S03 — 此特例與全稱證明分開。
- S06 · premise_audit · S04, S05 — 不依 K 是否母空間開或閉。
- S05 · premise_audit · S03, S04 — 窮盡三個相對開集才可此推論。
- S04 · premise_audit · S03 — j 依覆蓋選取，覆蓋並未固定為單一測試。
- S03 · premise_audit · S02 — 全集在此步已改為 K。
- S02 · premise_audit · G1, S01 — 相對開集見證不需包含於 K。
- S01 · premise_audit · G1 — 核的是完整四項族。





## 錯誤控制與反例

覆蓋在 K相對聯集要含 K，不需含 X。

原索引有限子覆蓋保留原族成員。


- {b} 單獨覆蓋 K。 → reject — c 未被覆蓋。
- 任何相對開集也在母空間開。 → reject — {b} 不屬母拓撲。
- 所有拓撲的緊緻等於閉且有界。 → reject — 本例未指定度量；一般結論需額外假設。





## 結論與限制

K 在誘導拓撲緊緻；相對開集為空集、{b}、K。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 56c43748460b659d5e4882ad8b91e59c79a448b72613dbffe32f07c5de2c09e5
- original source SHA-256: 56c43748460b659d5e4882ad8b91e59c79a448b72613dbffe32f07c5de2c09e5
- 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-01.json)