拉回覆蓋再推回索引

目標與範圍

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

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

已知條件與符號

• 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 — 連續性要求每個目標開集的逆像開；相對開集為母開集與子空間之交；緊緻表示每個相對開覆蓋有有限原索引子覆蓋；閉集有開補集。

逐步主鏈

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

\tau_X,\tau_Y\text{ are topologies}

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

\varnothing,X,X\in\tau_X

K=X=\{a,b\}

K\text{ is compact}

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))

W_i\in\tau_Y

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

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}

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

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

\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

局部子步與引理

本稿無局部子步。

逐步反向審查

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