# 有限乘積拓撲

有限多個拓撲空間的Cartesian product由open rectangles生成乘積拓撲。

mko-finite-product-topology · definition · v0.10.0



## 數學敘述

二因子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。





## 代表公式（精確 TeX）

P(X,Y)=t





## 成立條件


- 本節finite product限制至少一個因子；exact題族固定兩個非空factor，不主張零因子product convention。
- 兩個factor carrier有限且topology包含空集與全體並對任意聯集、有限交封閉。
- ordered pairs、rectangles與set-of-sets均以extensional canonical form核對。





## 符號作用域


- P — 有限乘積拓撲算子
- X — 第一拓撲空間
- Y — 第二拓撲空間
- t — 乘積拓撲





## 直觀、定義與常見誤解

factor topology與Cartesian carrier資格先核。

rectangle basis須再對任意聯集封閉。

projection與coordinate criterion只在完整生成拓撲上核對。

把basic rectangles直接當全部opens，或因有限情形而宣稱無限product等於box topology。





## 已採用的推導導讀

[四點乘積的全部開集](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-finite-product-topology-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [拓撲基底](https://ocme.evemisslab.com/zh-Hant/mko/mko-topological-basis/) — open rectangles生成拓撲。
- [拓撲空間](https://ocme.evemisslab.com/zh-Hant/mko/mko-topological-space/) — factor與product axioms。
- [集合運算](https://ocme.evemisslab.com/zh-Hant/mko/mko-set-operations/) — Cartesian carrier、聯集與交集。
- [二元關係與集合投影](https://ocme.evemisslab.com/zh-Hant/mko/mko-relation/) — ordered-pair carrier與coordinate maps。
- [拓撲連續映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-topological-continuity/) — projections與coordinate criterion。
- [函數合成](https://ocme.evemisslab.com/zh-Hant/mko/mko-composition/) — coordinate maps與universal property。





## 驗證界線

finite enumeration只證指定空間，不證一般product universal property。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

加入任意乘積、box topology與Tychonoff邊界。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/finite-product-topology.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-product-topology/index.md)