# 拓撲連續映射：在有限空間中用逆像判定連續，並與開映射區分

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

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

derivation-mko-topological-continuity-01 · production-20261019-adopted-96



## 目標與範圍

設 X={1,2,3}，τX={∅,{1},{1,2},X}；Y={a,b}，τY={∅,{a},Y}。對三個以完整表格給出的映射 f（1↦a、2↦a、3↦b）、g（1↦a、2↦b、3↦a）、c（全部 ↦b），用逆像條件判定是否連續，並判定是否為開映射；證明連續映射的合成仍連續並以 q:Y→Z 驗證；最後數出 X→Y 的全部連續映射。

在 MKO 範圍內工作：兩個底集合與拓撲固定（假設 a1），映射以完整總表給出，逆像收集所有映入目標子集的來源元素（假設 a2）。具體映射分類與計數只處理明示的有限拓撲；合成連續的一般引理則對任意拓撲空間證明，不使用有限性；不處理實函數的 ε-δ 連續、子空間或孤立點語義橋，不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- image_preimage_def
- function_def
- composition_def
- set_builder
- subset_def


- G1 — 來源空間：X={1,2,3}，τX={∅,{1},{1,2},X}（MKO 假設 a1）。
- G2 — 目標空間：Y={a,b}，τY={∅,{a},Y}（MKO 假設 a1）。
- G3 — 映射以完整總表給出（MKO 假設 a2）：f(1)=a、f(2)=a、f(3)=b；g(1)=a、g(2)=b、g(3)=a；c(1)=c(2)=c(3)=b。
- G4 — 第三個空間 Z={0,1}，τZ={∅,{0},Z}，以及映射 q:Y→Z，q(a)=0、q(b)=1。


- (X,\tau_X) — 來源空間 X={1,2,3}
- (Y,\tau_Y) — 目標空間 Y={a,b}
- h^{-1}[V] — V 在 h 下的逆像 {x∈X ∣ h(x)∈V}
- h[U] — U 在 h 下的像 {h(x) ∣ x∈U}
- f,g,c — 三個待判定的映射
- q:Y\to Z — 用來驗證合成的第二個映射





## 規則與來源


- image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- composition_def · prerequisite — 合成：對 f:A→B 與 g:B→C，g∘f:A→C 定義為 (g∘f)(a)=g(f(a))。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- topology_def · prerequisite — 拓撲：X 上的開集族 τ 包含 ∅ 與 X，對任意聯集與有限交集封閉。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- mko_topological_continuity_def · cited — 給定拓撲空間 (X,τX)、(Y,τY) 與總映射 f:X→Y，f 連續當且僅當對每個 V∈τY，逆像 f⁻¹[V]∈τX。這是逆像條件，不要求開集的像為開。 · mko-topological-continuity
- mko_topological_space_def · cited — X 上的拓撲是子集合族 τ⊆P(X)，滿足 ∅∈τ、X∈τ、任意子族的聯集在 τ、任意有限子族的交集在 τ（空族聯集為 ∅，空族交集為 X）。 · mko-topological-space
- open_map_def · prerequisite — 映射 h:X→Y 稱為開映射，若對每個 U∈τX，像 h[U]∈τY。
- finite_exhaustion · prerequisite — 對明示列出的有限集合 D，∀V∈D, Q(V) 等價於 Q 對每個列出元素都成立的合取；只檢查部分元素不足以證明它，一個不成立的元素就否定它。
- L_chain · lemma — 若集合 S 的一個有限子集合族含 ∅ 與 S，且任兩個成員都可用 ⊆ 比較（全序），則它是 S 上的拓撲。
- L_trivial_preimage · lemma — 對每個總映射 h:X→Y，h⁻¹[∅]=∅ 且 h⁻¹[Y]=X。
- L_comp_preimage · lemma — 對 h:X→Y、k:Y→Z 與 W⊆Z，(k∘h)⁻¹[W]=h⁻¹[k⁻¹[W]]。





## 逐步主鏈

S01 · theorem_application操作前

\tau_X,\ \tau_Y,\ \tau_Z

操作後

\text{each is a topology on}\ X,\ Y,\ Z

條件：\varnothing\subseteq\{1\}\subseteq\{1,2\}\subseteq X; \varnothing\subseteq\{a\}\subseteq Y; \varnothing\subseteq\{0\}\subseteq Z

規則：L_chain · 依賴：G1, G2, G4

葉節點依據：topology_def + subset_def

三個族都是有限的、含空集與全集，而且成員排成一條包含鏈：∅⊆{1}⊆{1,2}⊆X，∅⊆{a}⊆Y，∅⊆{0}⊆Z。依引理 L_chain（在 S01.1 證明），三者都是拓撲。連續性的定義需要兩端都是拓撲空間，所以先確認這點。



S02 · equivalent操作前

h:X\to Y\ \text{continuous}

操作後

h^{-1}[\varnothing]\in\tau_X\ \wedge\ h^{-1}[\{a\}]\in\tau_X\ \wedge\ h^{-1}[Y]\in\tau_X

條件：\tau_Y=\{\varnothing,\{a\},Y\}

規則：finite_exhaustion · 依賴：S01, G2, mko_topological_continuity_def

葉節點依據：def_unfold + finite_exhaustion

展開 MKO 定義：h 連續當且僅當對每個 V∈τY，h⁻¹[V]∈τX。τY 只有三個成員，所以這個全稱條件等價於三個成員條件的合取。判定連續必須檢查目標的每一個開集，不能只抽查一個。



S03 · equivalent操作前

h^{-1}[\varnothing]\in\tau_X\wedge h^{-1}[\{a\}]\in\tau_X\wedge h^{-1}[Y]\in\tau_X

操作後

h\ \text{continuous}\iff h^{-1}[\{a\}]\in\tau_X

條件：h\ \text{total}

規則：L_trivial_preimage · 依賴：S02, G1

葉節點依據：and_intro_elim + image_preimage_def + topology_def

依引理 L_trivial_preimage（在 S03.1 證明），任何總映射都有 h⁻¹[∅]=∅∈τX 與 h⁻¹[Y]=X∈τX，所以這兩個條件自動成立。唯一有資訊量的是 V={a}：h 連續當且僅當 h⁻¹[{a}]∈τX。這也說明為什麼只查 ∅ 或 Y 永遠查不出不連續。



S04 · implies操作前

f^{-1}[\{a\}]=\{x\in X\mid f(x)=a\}

操作後

f^{-1}[\{a\}]=\{1,2\}

條件：無

規則：image_preimage_def · 依賴：G3

葉節點依據：image_preimage_def + set_builder

逐列掃描 f 的完整表：f(1)=a 收入、f(2)=a 收入、f(3)=b 不收。逆像要收集所有映到 a 的來源元素，不能只找一個。



S05 · implies操作前

f^{-1}[\{a\}]=\{1,2\}

操作後

\{1,2\}\in\tau_X\ \Rightarrow\ f\ \text{continuous};\quad f\ \text{is an open map}

條件：無

規則：mko_topological_continuity_def · 依賴：S03, S04, G1, G3, open_map_def

葉節點依據：mko_topological_continuity_def + and_intro_elim + open_map_def

{1,2} 是 τX 的成員，依 S03 的等價，f 連續。三個開集的逆像分別是 ∅、{1,2}、X，全在 τX 中。 另對全部四個來源開集逐一取像：f[∅]=∅、f[{1}]={a}、f[{1,2}]={a}、f[X]=Y；四個像都屬於 τY，依開映射定義，f 也是開映射。



S06 · implies操作前

g^{-1}[\{a\}]=\{x\in X\mid g(x)=a\}

操作後

g^{-1}[\{a\}]=\{1,3\}

條件：無

規則：image_preimage_def · 依賴：G3

葉節點依據：image_preimage_def + set_builder

掃描 g 的表：g(1)=a 收入、g(2)=b 不收、g(3)=a 收入，得 {1,3}。



S07 · implies操作前

g^{-1}[\{a\}]=\{1,3\}

操作後

\{1,3\}\notin\tau_X\ \Rightarrow\ g\ \text{not continuous}

條件：無

規則：quantifier_negation · 依賴：S03, S06, G1

葉節點依據：quantifier_negation + finite_exhaustion

{1,3} 不等於 τX 的四個成員中的任何一個，所以不是開集。開集 {a} 的逆像不開，依量詞否定，「對每個 V∈τY 逆像都開」不成立，g 不連續。



S08 · implies操作前

g[U]\ \text{for}\ U\in\tau_X

操作後

g[\varnothing]=\varnothing,\ g[\{1\}]=\{a\},\ g[\{1,2\}]=Y,\ g[X]=Y\ \in\tau_Y

條件：無

規則：open_map_def · 依賴：G1, G2, G3

葉節點依據：open_map_def + image_preimage_def + finite_exhaustion

計算 g 對每個來源開集的像：∅ 的像是 ∅；{1} 的像是 {a}；{1,2} 的像是 {a,b}=Y；X 的像是 {a,b}=Y。四個像都在 τY，所以 g 是開映射。但 S07 已證 g 不連續：開集的像為開，不等於連續（MKO 第三段）。



S09 · implies操作前

c^{-1}[\{a\}]=\{x\mid c(x)=a\}

操作後

c^{-1}[\{a\}]=\varnothing\in\tau_X\ \Rightarrow\ c\ \text{continuous}

條件：無

規則：mko_topological_continuity_def · 依賴：S03, G3, G1

葉節點依據：image_preimage_def + mko_topological_continuity_def

c 把每個點送到 b，沒有點映到 a，所以 c⁻¹[{a}]=∅∈τX。依 S03，c 連續。逆像不需要 c 有反函數：c 不是單射，c⁻¹[{a}] 仍是定義良好的集合。



S10 · implies操作前

c[X]

操作後

c[X]=\{b\}\notin\tau_Y\ \Rightarrow\ c\ \text{not open}

條件：無

規則：quantifier_negation · 依賴：G1, G2, G3

葉節點依據：quantifier_negation + open_map_def + image_preimage_def

X 是開集，其像 c[X]={b} 不在 τY={∅,{a},Y} 中，所以 c 不是開映射。c 連續但不開；與 S07、S08 的 g 合起來，連續與開映射兩個方向都互不蘊含。



S11 · theorem_application操作前

h:X\to Y,\ k:Y\to Z\ \text{continuous},\ W\in\tau_Z

操作後

(k\circ h)^{-1}[W]=h^{-1}[k^{-1}[W]]\in\tau_X\ \Rightarrow\ k\circ h\ \text{continuous}

條件：無

規則：L_comp_preimage · 依賴：mko_topological_continuity_def

葉節點依據：composition_def + image_preimage_def + forall_intro

設 h、k 連續，W∈τZ。依引理 L_comp_preimage（在 S11.1 證明），(k∘h)⁻¹[W]=h⁻¹[k⁻¹[W]]。k 連續給 k⁻¹[W]∈τY，h 連續再給 h⁻¹[k⁻¹[W]]∈τX。W 是任意開集，所以 k∘h 連續。這對任何拓撲空間都成立，不限於有限情形。



S12 · implies操作前

q^{-1}[\{0\}]=\{a\}\in\tau_Y,\ f\ \text{continuous}

操作後

(q\circ f)^{-1}[\{0\}]=f^{-1}[\{a\}]=\{1,2\}\in\tau_X

條件：無

規則：forall_elim · 依賴：S11, S05, G4, G3

葉節點依據：forall_elim + composition_def + image_preimage_def

q 連續：q⁻¹[{0}]={a}∈τY，另兩個逆像依 L_trivial_preimage 自動是開集。依 S11，q∘f 連續，且 (q∘f)⁻¹[{0}]=f⁻¹[q⁻¹[{0}]]=f⁻¹[{a}]={1,2}。直接重算：q∘f 把 1、2 送到 0，把 3 送到 1，所以 (q∘f)⁻¹[{0}]={1,2}∈τX。兩種算法一致。



S13 · implies操作前

h\mapsto A_h=h^{-1}[\{a\}]\ \text{for}\ h:X\to Y

操作後

\#\{h:X\to Y\}=2^3=8,\ \#\{h\ \text{continuous}\}=|\tau_X|=4

條件：無

規則：injective_surjective_def · 依賴：S03, G1

葉節點依據：injective_surjective_def + finite_counting_basics + numeric_evaluation

每個映射 h:X→Y 由集合 A_h=h⁻¹[{a}] 唯一決定（x∈A_h 時 h(x)=a，否則 h(x)=b），反之每個子集 A⊆X 都給出一個映射，所以 h↦A_h 是映射與子集之間的雙射，共 2^3=8 個映射。依 S03，h 連續當且僅當 A_h∈τX，所以恰有 |τX|=4 個連續映射：A=∅（即 c）、A={1}、A={1,2}（即 f）、A=X（常值 a）。g 對應 A={1,3}，不在其中。







## 局部子步與引理

S01.1 · implies操作前

\mathcal{F}\ \text{a finite chain},\ \varnothing,S\in\mathcal{F},\ F\subseteq\mathcal{F}

操作後

\textstyle\bigcup F\in\mathcal{F},\ \bigcap F\in\mathcal{F}

條件：無

規則：nat_induction · 依賴：nat_induction, set_operations_def, subset_def

葉節點依據：nat_induction + set_operations_def + subset_def

族有限，所以每個子族 F 有限。F 為空時，∪F=∅ 與 ∩F=S 都在族中。F 非空時，對成員數歸納可知有限的全序子族有最大成員 M 與最小成員 m（新加入的成員與舊的最大、最小者可比較）。所有成員都包含於 M，且都包含 m，所以 ∪F=M、∩F=m，都在族中。故族對每個子族的聯集與交集封閉，是拓撲，證得 L_chain。



S03.1 · implies操作前

x\in h^{-1}[\varnothing],\ x\in h^{-1}[Y]

操作後

h^{-1}[\varnothing]=\varnothing,\ h^{-1}[Y]=X

條件：h\ \text{total}

規則：image_preimage_def · 依賴：image_preimage_def, function_def

葉節點依據：image_preimage_def + function_def + set_extensionality

x∈h⁻¹[∅] 表示 h(x)∈∅，對任何 x 都不成立，所以 h⁻¹[∅]=∅。x∈h⁻¹[Y] 表示 h(x)∈Y；因為 h 是總映射，每個 x∈X 都有 h(x)∈Y，所以 h⁻¹[Y]=X。證得 L_trivial_preimage。



S11.1 · equivalent操作前

x\in(k\circ h)^{-1}[W]

操作後

x\in h^{-1}[k^{-1}[W]]

條件：無

規則：image_preimage_def · 依賴：composition_def, image_preimage_def

葉節點依據：composition_def + image_preimage_def + set_extensionality

x∈(k∘h)⁻¹[W] ⇔ (k∘h)(x)∈W ⇔ k(h(x))∈W ⇔ h(x)∈k⁻¹[W] ⇔ x∈h⁻¹[k⁻¹[W]]。每一步都是定義的展開，依集合外延性兩集合相等，證得 L_comp_preimage。







## 逐步反向審查


- S13 · premise_audit · S03, injective_surjective_def, finite_counting_basics — 計數依賴雙射與 S03 的等價；這是完整列舉，不是抽樣（N1、N2、N3）。
- S12 · premise_audit · S11, S05, G4, L_trivial_preimage — 這是一般結論的一個實例並附直接重算；一個實例不能反過來證明一般結論。
- S11.1 · inverse_equivalence · composition_def, image_preimage_def, set_extensionality — 每一步都是定義的等價改寫，兩向成立。注意逆像的順序是先 k 後 h，與合成順序相反。
- S11 · premise_audit · L_comp_preimage, mko_topological_continuity_def, forall_intro — 需要兩個映射都連續；不宣稱反向（k∘h 連續不推出 h 或 k 連續）。
- S10 · premise_audit · G2, open_map_def, quantifier_negation — 一個來源開集的像不開就足以否定開映射。
- S09 · premise_audit · S03, G3, image_preimage_def — 逆像記號不預設反函數存在（image_preimage_def）；結論只需 ∅∈τX。
- S08 · premise_audit · G3, open_map_def, image_preimage_def — 開映射也是對所有來源開集的全稱條件，四個都已檢查。此步不宣稱開映射與連續有任何蘊含關係。
- S07 · premise_audit · S06, G1, quantifier_negation, finite_exhaustion — 一個反例 V={a} 就足以否定全稱條件；判定 {1,3}∉τX 需要與四個成員逐一比較。
- S06 · premise_audit · G3, image_preimage_def — 三列都已檢查。
- S05 · sufficient_goal_reduction · S03, S04, G1, G3, open_map_def — 目標：f 連續。依 S03 足夠且必要的條件是 f⁻¹[{a}]∈τX，由 S04 與 τX 的列表正向得到。 開映射部分另以 G3 的完整映射表驗全部四個來源開集之像，依 open_map_def 得證。
- S04 · premise_audit · G3, image_preimage_def, set_builder — 需要完整表的三列都檢查過；漏掉一列就可能得到錯誤的逆像。
- S03.1 · premise_audit · image_preimage_def, function_def — 第二個等式需要 h 是總映射；若某些 x 沒有值，h⁻¹[Y] 會小於 X。
- S03 · inverse_equivalence · L_trivial_preimage, mko_topological_space_def — 把兩個恆真的合取項去掉不改變真假，兩向成立；需要 ∅、X∈τX。
- S02 · inverse_equivalence · mko_topological_continuity_def, finite_exhaustion — 有限全稱與合取互相等價，兩向都成立。條件是逆像屬於 τX，不是像屬於 τY。
- S01.1 · premise_audit · nat_induction, set_operations_def, subset_def, mko_topological_space_def — 需要有限性（最大最小元存在）與可比較性；兩者缺一，結論可能失敗。
- S01 · premise_audit · G1, G2, G4, L_chain — 需要三個族的完整列表與鏈條件；不是每個有限族都是拓撲，鏈只是一個充分條件。





## 錯誤控制與反例

開集的像為開不是連續MKO 指出的誤解是把「開集的像為開」當作連續的定義。g 把每個開集映成開集，卻不連續（S07、S08）；c 連續卻把開集 X 映成不開的 {b}（S09、S10）。連續性只看逆像。

只抽查一個開集不夠∅ 與 Y 的逆像對任何總映射都是開集（S03），所以只查它們永遠會「通過」；g 正是如此。必須檢查 τY 的每一個成員，關鍵的是 {a}。

逆像不需要反函數c 不是單射，沒有反函數，但 c⁻¹[{a}]=∅ 與 c⁻¹[{b}]=X 都是定義良好的集合。把 f⁻¹ 讀成反函數會讓人誤以為非單射映射無法判定連續。


- g 把每個開集映成開集，所以 g 連續 → reject — g⁻¹[{a}]={1,3}∉τX。
- g⁻¹[∅]=∅ 與 g⁻¹[Y]=X 都是開集，所以 g 連續 → reject — 這兩個逆像對任何總映射都開；必須檢查 {a}，而 g⁻¹[{a}]={1,3} 不開。
- c 連續，所以 c 把開集映成開集 → reject — c[X]={b}∉τY。
- c 不是單射，c⁻¹ 不存在，所以無法判定 c 是否連續 → reject — 逆像不需要反函數：c⁻¹[{a}]=∅∈τX，c 連續。





## 結論與限制

f 連續且為開映射（全部來源開集的像為 ∅、{a}、{a}、Y；f⁻¹[{a}]={1,2}∈τX）；g 不連續（g⁻¹[{a}]={1,3}∉τX），但 g 是開映射；c 連續（c⁻¹[{a}]=∅），但 c 不是開映射（c[X]={b}∉τY）。連續映射的合成仍連續，q∘f 為例。X→Y 共 8 個映射，其中恰有 4 個連續。


- 與 Mathlib Continuous 的開集逆像定義、實函數 ε-δ 連續、子空間與孤立點的語義橋（MKO formal next）未在此建立。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: b117526fa854e48680a3b666c42aa17e7e65e805f5d983e78d1584911010c82d
- original source SHA-256: 6d48e6785097f15248cf83e69efa2ae7a0fd26ea5e6dd4144f0d3eb785992398
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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