# 兩個有限鏈狀空間的同胚

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

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

derivation-mko-homeomorphism-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

用全部逆像核對重命名映射是同胚。

完整有限拓撲；不宣稱等距、可微或幾何全等。





## 已知條件與符號


- sets
- topology
- definition_here


- G1 — X={a,b,c}, tau_X={空集,{a},{a,b},X}；Y={u,v,w}, tau_Y={空集,{u},{u,v},Y}。
- G2 — h(a)=u,h(b)=v,h(c)=w。


- h — 重命名映射
- k — 反函數





## 規則與來源


- mko_definition · cited — 有限拓撲題完整列出來源與目標拓撲，逐一核目標開集的逆像及反向責任。有限離散空間任意雙射為同胚只限該範圍；同胚不升格成等距、可微或幾何全等。 · mko-homeomorphism
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。
- definition_here · prerequisite — 雙射的逆函數滿足兩個合成皆恆等；同胚是雙射且正反函數都連續；連續以全部開集逆像為開定義。





## 逐步主鏈

S01 · implies操作前

\tau_X,\tau_Y\text{ are finite inclusion chains}

操作後

\tau_X,\tau_Y\text{ satisfy all topology axioms}

條件：無

規則：topology · 依賴：G1

葉節點依據：topology

各族含空集全集，任意聯及有限交仍是鏈中的極端項。



S02 · implies操作前

h:a\mapsto u,\ b\mapsto v,\ c\mapsto w

操作後

h\text{ is total and bijective}

條件：無

規則：sets · 依賴：G1, G2

葉節點依據：sets

三個來源各有一值，三個像互異且耗盡 Y。



S03 · equivalent操作前

h^{-1}(\varnothing),\ h^{-1}(\{u\})

操作後

\varnothing,\ \{a\}

條件：無

規則：sets · 依賴：G2

葉節點依據：sets

逐點讀表得到目標前兩個開集的逆像。



S04 · implies操作前

h^{-1}(\{u,v\}),\ h^{-1}(Y)

操作後

\{a,b\},\ X

條件：無

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

葉節點依據：definition_here

後兩個逆像也在 tau_X；四個目標開集皆已核完，故 h 連續。



S05 · definition操作前

k=h^{-1}

操作後

k(u)=a,\ k(v)=b,\ k(w)=c

條件：無

規則：definition_here · 依賴：S02

葉節點依據：definition_here

由雙射逐項建構逆函數，滿足 k h 與 h k 都是恆等。



S06 · implies操作前

k^{-1}(\varnothing),k^{-1}(\{a\}),k^{-1}(\{a,b\}),k^{-1}(X)

操作後

\varnothing,\{u\},\{u,v\},Y

條件：無

規則：definition_here · 依賴：G1, S05, definition_here

葉節點依據：definition_here

完整核四個來源開集對 k 的逆像，都在 tau_Y，故逆函數連續。



S07 · definition操作前

h\text{ bijective},\quad h,k\text{ continuous}

操作後

h\text{ is a homeomorphism}

條件：無

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

葉節點依據：definition_here

三個責任合在一起才符合定義。



S08 · implies操作前

A=\{a,b\}\in\tau_X

操作後

h(A)=\{u,v\}\in\tau_Y

條件：無

規則：sets · 依賴：G1, S07

葉節點依據：sets

以一個開集像回讀核對結構；一般開性由逆函數連續已證。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S07 — 這個特例不是 S06 全部逆像核對的替代。
- S07 · premise_audit · S02, S04, S06 — 此結論保存開集結構，不附送任何未指定距離資料。
- S06 · premise_audit · G1, S05, definition_here — 並未由 h 連續與雙射直接跳到逆連續。
- S05 · premise_audit · S02 — 先前雙射前提讓此反函數合法。
- S04 · premise_audit · G1, G2, definition_here — 連續性不是僅核單點的映射值，而是全部開集逆像。
- S03 · inverse_equivalence · G2 — 逆像是 X 的子集，與反函數的方向不要混淆。
- S02 · premise_audit · G1, G2 — 因此逆函數三項也有唯一指定。
- S01 · premise_audit · G1 — 兩邊公理各自核對，不能只因點數相同就假定。





## 錯誤控制與反例

兩個方向分別核 h 與反函數的全部開集逆像。

結構不升格同胚不等於等距、可微或剛體全等。


- 同點數空間的每個雙射都是同胚。 → reject — 從具離散拓撲的兩點空間到只以空集、全集為開集的兩點空間，其恆等雙射連續，但逆映射不連續。
- h 自動是等距映射。 → reject — 本題未給度量，且同胚只核拓撲。
- 只核 h^{-1}({u}) 就完成連續性。 → reject — 需核全部目標開集。





## 結論與限制

h 是這兩個指定有限拓撲間的同胚。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 569c899605b872432df600bc9e60f4e0a755fcd15015d67a2f0f72cb11dbe8dc
- original source SHA-256: c108be020f742133584c559dbb70070aa0c7766974d449f9c8a8484a251835dc
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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