# 拉回覆蓋再推回索引

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

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

derivation-mko-continuous-image-of-compact-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

以明示有限映射呈現緊緻像的覆蓋論證。

完整有限拓撲，同時解釋任意目標覆蓋的拉回；不推反命題。





## 已知條件與符號


- sets
- topology
- definition_here


- G1 — X={a,b}, tau_X={空集,{a},{b},X}; Y={u,v}, tau_Y={空集,{u},Y}; K=X。
- G2 — f(a)=f(b)=u。


- W_i — 像的目標開覆蓋
- J — 保留的原索引





## 規則與來源


- mko_definition · cited — 對f(K)的ambient-open cover取逆像，continuity使逆像open且覆蓋K；K的finite subcover再推回覆蓋f(K)。不需要injective或surjective。compact image不反推domain compact；compact preimage或image closed也各需額外假設（後者常需Hausdorff）。 · mko-continuous-image-of-compact
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。
- definition_here · prerequisite — 連續性要求每個目標開集的逆像開；相對開集為母開集與子空間之交；緊緻表示每個相對開覆蓋有有限原索引子覆蓋；閉集有開補集。





## 逐步主鏈

S01 · implies操作前

\tau_X=\mathcal P(X),\quad\varnothing\subset\{u\}\subset Y

操作後

\tau_X,\tau_Y\text{ are topologies}

條件：無

規則：topology · 依賴：G1

葉節點依據：topology

來源是全部子集；目標是含兩端的有限鏈，兩邊公理均成立。



S02 · implies操作前

f^{-1}(\varnothing),f^{-1}(\{u\}),f^{-1}(Y)

操作後

\varnothing,X,X\in\tau_X

條件：無

規則：definition_here · 依賴：G1, G2, S01, definition_here

葉節點依據：definition_here

核全部目標開集的逆像，所以 f 連續。



S03 · implies操作前

K=X=\{a,b\}

操作後

K\text{ is compact}

條件：無

規則：definition_here · 依賴：G1, definition_here

葉節點依據：definition_here

對任意覆蓋分別選含 a 與含 b 的原成員，至多兩個便覆蓋 K。



S04 · implies操作前

f(K)=\{u\}\subseteq\bigcup_{i\in I}W_i,\quad W_i\in\tau_Y

操作後

K\subseteq\bigcup_{i\in I}(K\cap f^{-1}(W_i))

條件：無

規則：sets · 依賴：G2, S02

葉節點依據：sets

任取像的目標開覆蓋；每個 x∈K 的像被某個 W_i 覆蓋，所以逆像覆蓋 K。



S05 · implies操作前

W_i\in\tau_Y

操作後

K\cap f^{-1}(W_i)\text{ is relatively open in }K

條件：無

規則：definition_here · 依賴：S02, S04, definition_here

葉節點依據：definition_here

連續性給母逆像開，相交 K 就相對開。



S06 · theorem_application操作前

K\subseteq\bigcup_{i\in I}(K\cap f^{-1}(W_i))

操作後

K\subseteq\bigcup_{i\in J}f^{-1}(W_i),\quad J\subseteq I\text{ finite}

條件：無

規則：definition_here · 依賴：S03, S04, S05, definition_here

葉節點依據：definition_here

用 K 的緊緻性取得有限的原索引子集 J。



S07 · implies操作前

z\in f(K),\ z=f(x),\ x\in K

操作後

z\in\bigcup_{i\in J}W_i

條件：無

規則：sets · 依賴：S06

葉節點依據：sets

x 被某個選定逆像覆蓋，所以同一 i 的 W_i 包含 z；索引原樣推回。



S08 · implies操作前

\forall(W_i)\text{ covering }f(K),\ \exists J\text{ finite covering }f(K)

操作後

f(K)=\{u\}\text{ is compact but not closed in }Y

條件：無

規則：definition_here · 依賴：S04, S07, definition_here

葉節點依據：definition_here

前半完成緊緻定義；後半因補集 {v} 不開而不閉，提醒未給 Hausdorff 不能宣稱閉像。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S04, S07, definition_here — 緊緻與閉性由不同責任判斷。
- S07 · premise_audit · S06 — 沒有用 f(逆像)=W_i 的錯誤等式；只需包含關係。
- S06 · premise_audit · S03, S04, S05, definition_here — J 的有限性來自已證緊緻性，不是預設 I 有限。
- S05 · premise_audit · S02, S04, definition_here — 開性前提不能由覆蓋性代替。
- S04 · premise_audit · G2, S02 — 只用像點屬性，未要求 f 對全部 Y 滿射。
- S03 · premise_audit · G1, definition_here — 有限選取對所有覆蓋適用，不是單一覆蓋成功。
- S02 · premise_audit · G1, G2, S01, definition_here — 不需要 f 單射或滿射，實際上兩者皆不成立。
- S01 · premise_audit · G1 — 沒有省略任一目標開集。





## 錯誤控制與反例

逆像而非開像用連續性的逆像責任拉回覆蓋。

索引不變J 從目標原覆蓋取得且原樣推回。


- 定理需要 f 單射。 → reject — 本例兩點同像仍已證像緊緻。
- 緊緻像推出原空間緊緻。 → reject — 常值映射 (0,1)→{u} 的像緊緻；開覆蓋 (1/n,1)（n≥2）證來源不緊緻。
- 所有連續緊緻像都閉。 → reject — 本例 {u} 的補集 {v} 不開。





## 結論與限制

連續像 {u} 緊緻但在本非 Hausdorff 目標不閉。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: d6eaece8c24bc185ce8421028d38a700da364006b5f47dd2476ede583c0cbbbc
- original source SHA-256: d6eaece8c24bc185ce8421028d38a700da364006b5f47dd2476ede583c0cbbbc
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-continuous-image-of-compact-01.json)