# 四點乘積的全部開集

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

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

derivation-mko-finite-product-topology-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

由兩個 Sierpinski 因子生成全部乘積開集並核投影。

固定兩個非空有限因子；不處理零因子或外推無限 box 拓撲。





## 已知條件與符號


- sets
- topology
- definition_here


- G1 — X=Y={0,1}，兩因子拓撲皆 {空集,{0},{0,1}}；a=(0,0),b=(0,1),c=(1,0),d=(1,1),P={a,b,c,d}。


- P — Cartesian 載體
- \mathcal B — 矩形基底
- \pi_i — 座標投影





## 規則與來源


- mko_definition · cited — 二因子finite models先驗每個factor topology，再建立完整Cartesian carrier與全部U×V basic rectangles，取任意聯集生成product topology。投影preimages必為open；對有限source Z，map z↦(f(z),g(z))連續恰當兩個coordinate maps連續。有限乘積與box topology相同，不能把這點外推到無限乘積；任意一族rectangles本身通常不是完整topology。 · mko-finite-product-topology
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。
- definition_here · prerequisite — Cartesian 載體由有序對構成；乘積開集為任意開矩形聯；投影取指定座標；連續表示每個目標開集逆像開。





## 逐步主鏈

S01 · implies操作前

\varnothing\subset\{0\}\subset\{0,1\}

操作後

\tau_X,\tau_Y\text{ are topologies}

條件：無

規則：topology · 依賴：G1

葉節點依據：topology

三項鏈含兩端且聯交封閉，兩因子各自合法。



S02 · definition操作前

P=X\times Y

操作後

P=\{a,b,c,d\},\quad |P|=2\cdot2=4

條件：無

規則：definition_here · 依賴：G1

葉節點依據：definition_here

完整 Cartesian 載體包含四個有序對。



S03 · definition操作前

U\times V,\quad U\in\tau_X,V\in\tau_Y

操作後

\mathcal B=\{\varnothing,\{a\},\{a,b\},\{a,c\},P\}

條件：無

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

葉節點依據：definition_here

九個矩形去重成五項；任一因子空給空，四個非空組合如列。



S04 · definition操作前

\tau_P=\{\bigcup\mathcal C:\mathcal C\subseteq\mathcal B\}

操作後

\tau_P=\{\varnothing,\{a\},\{a,b\},\{a,c\},\{a,b,c\},P\}

條件：無

規則：definition_here · 依賴：S03

葉節點依據：definition_here

兩個不可比較矩形的聯新增 {a,b,c}；其餘聯給已列項，故六項完整。



S05 · implies操作前

\{a,b\}\cap\{a,c\}=\{a\},\quad \{a,b\}\cup\{a,c\}=\{a,b,c\}

操作後

\tau_P\text{ is a topology}

條件：無

規則：topology · 依賴：S04

葉節點依據：topology

除這對不可比較集外皆按包含取交聯；與新增三點集相交聯也留在清單，端點均在。



S06 · implies操作前

\pi_1^{-1}(\{0\})=\{a,b\},\quad\pi_2^{-1}(\{0\})=\{a,c\}

操作後

\pi_1,\pi_2\text{ are continuous}

條件：無

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

葉節點依據：definition_here

另兩個因子開集為空與全體，逆像是空與 P，所以全部逆像開。



S07 · implies操作前

h(z)=(f(z),g(z)),\quad f,g\text{ continuous}

操作後

h^{-1}(U\times V)=f^{-1}(U)\cap g^{-1}(V)\text{ open}

條件：f:Z\to X,\ g:Z\to Y\text{ continuous}

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

葉節點依據：definition_here

對任意有拓撲的有限來源 Z，連續座標的逆像交開；再對任意矩形聯取逆像聯。



S08 · implies操作前

h\text{ continuous}

操作後

f=\pi_1\circ h,\quad g=\pi_2\circ h\text{ continuous}

條件：h:Z\to P\text{ continuous}

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

葉節點依據：definition_here

連續映射合成連續，因逆像是連續逆像的合成；結合前步得座標判準。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S06, S07, definition_here — 判準針對完整六項乘積拓撲，不是未封閉矩形清單。
- S07 · premise_audit · S03, S04, definition_here — 需先核 Z 的拓撲與兩座標連續，這是條件命題。
- S06 · premise_audit · G1, S04, definition_here — 每個投影的全部三個目標開集已核完。
- S05 · premise_audit · S04 — 有限族的任意聯可重複二元聯完成，已涵蓋全部。
- S04 · premise_audit · S03 — 特別核新增項並非矩形，避免漏聯。
- S03 · premise_audit · G1, S01, S02 — 尚未把矩形族直接稱完整拓撲。
- S02 · premise_audit · G1 — (0,1) 與 (1,0) 不合併。
- S01 · premise_audit · G1 — 有序點對的兩座標型別固定。





## 錯誤控制與反例

聯閉包先建矩形，再取全部聯，不能停在基底。

型別與方向投影逆像來自對應座標開集。


- 全部開集恰為五個矩形。 → reject — {a,b,c} 是兩矩形之聯且不是矩形。
- Cartesian 對不分順序。 → reject — b 與 c 是不同點。
- 有限 product=box 表示無限亦相同。 → reject — 在可數無限乘積 R^ℕ（所有實數序列），box 開集 ∏_{n∈ℕ}(-1,1) 非 product-open：任何含零的基本 product 鄰域只限制有限座標，可把未限制座標改成 2。





## 結論與限制

乘積拓撲恰六項，兩投影連續；有限來源的成對映射具座標連續判準。







## 驗證及來源綁定

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


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

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