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

目標與範圍

設 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]]。

逐步主鏈

\tau_X,\ \tau_Y,\ \tau_Z

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

c[X]

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

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}

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

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

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

局部子步與引理

\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}

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

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

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

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

逐步反向審查

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