# 有限拓撲的全稱緊緻證書

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

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

derivation-mko-compact-topological-space-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

證明三點鏈狀拓撲對每個開覆蓋都有有限子覆蓋。

有限空間的全稱論證，另核指定覆蓋；不分類無限空間。





## 已知條件與符號


- sets
- topology
- definition_here


- G1 — X={a,b,c}，tau={空集,{a},{a,b},X}；覆蓋可為任意索引族 (U_i)_{i∈I}。


- I — 任意覆蓋索引集
- J — 有限原索引子集





## 規則與來源


- mko_definition · cited — 本輪完整驗證有限carrier/topology並使用有限性全稱定理：open family本身有限，故任何cover已有有限subcover。另核 supplied cover，但單一cover成功不證一般或無限空間compact。 · mko-compact-topological-space
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。
- definition_here · prerequisite — 緊緻：對每個索引開覆蓋 (U_i)_{i∈I}，存在有限 J⊆I 使原成員 (U_j)_{j∈J} 仍覆蓋全空間。





## 逐步主鏈

S01 · implies操作前

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

操作後

\tau\text{ is a complete topology with }4\text{ members}

條件：無

規則：topology · 依賴：G1

葉節點依據：topology

有限鏈含兩端，非空聯交取最大最小項，核得全部拓撲公理。



S02 · implies操作前

X=\bigcup_{i\in I}U_i,\quad U_i\in\tau

操作後

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

條件：無

規則：sets · 依賴：G1, S01

葉節點依據：sets

對任意覆蓋，c 必被某個原成員覆蓋。



S03 · implies操作前

c\in U_j\in\tau

操作後

U_j=X

條件：無

規則：sets · 依賴：S01, S02

葉節點依據：sets

完整四項清單中只有 X 含 c。



S04 · implies操作前

J=\{j\}\subseteq I

操作後

\bigcup_{i\in J}U_i=X,\quad |J|=1

條件：無

規則：sets · 依賴：S03

葉節點依據：sets

保留原索引 j，得到一項的有限子覆蓋。



S05 · definition操作前

\forall\text{ open covers }(U_i)_{i\in I},\ \exists J\subseteq I\text{ finite}

操作後

X\text{ is compact}

條件：無

規則：definition_here · 依賴：S02, S04

葉節點依據：definition_here

覆蓋最初任意，故不是僅對一次覆蓋成功，而是完成緊緻定義。



S06 · implies操作前

D=\{U_i:i\in I\}\subseteq\tau

操作後

|D|\le4

條件：無

規則：sets · 依賴：S01

葉節點依據：sets

另一種一般有限族證法是對不同開集去重，再各選一個原索引。



S07 · implies操作前

(\{a\},\{a,b\},X)

操作後

\{X\}\text{ is a subcover of this supplied cover}

條件：無

規則：sets · 依賴：S01

葉節點依據：sets

指定三項覆蓋回讀第三項，與全稱證書相容但不取代它。



S08 · implies操作前

X=\varnothing\text{ in the empty-space boundary}

操作後

J=\varnothing\text{ covers }X

條件：無

規則：sets · 依賴：S05

葉節點依據：sets

空空間以空子覆蓋滿足同一定義，明示邊界慣例。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S05 — 只處理空載體的獨立邊界，未把本例 X 換掉。
- S07 · premise_audit · S01 — 這一步特例和 S05 的全稱結論來自不同層級。
- S06 · premise_audit · S01 — 任意多次重複不會增加不同開集的數目。
- S05 · premise_audit · S02, S04 — 關鍵前提是任意性，不能由一次數值成功反推。
- S04 · premise_audit · S03 — 沒有用不在原族的集合替換 U_j。
- S03 · premise_audit · S01, S02 — 這是窮盡開集後的結論，非單一成員抽查。
- S02 · premise_audit · G1, S01 — 選出的 j 可以依覆蓋而變，符合每覆蓋存在子覆蓋的量詞。
- S01 · premise_audit · G1 — 完整族的有限性已核，不是有限抽樣。





## 錯誤控制與反例

全稱入口先固定任意覆蓋，再選依覆蓋而定的原索引。

有限與抽樣完整有限拓撲的證書不是有限測試推一般結論。


- 抽查三個覆蓋足以證任意空間緊緻。 → reject — 未遍及所有覆蓋。
- 原覆蓋不含 X 也可任意把 X 加進子覆蓋。 → reject — 子覆蓋必選原成員；此例是先證原族實含 X。
- 有限開集樣本代表完整無限空間拓撲。 → reject — 有限完整性是本證書前提，不可外推。





## 結論與限制

此完整有限拓撲緊緻；證明對任意索引覆蓋成立。







## 驗證及來源綁定

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


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