子空間拓撲
Y⊆X的相對拓撲由全部母空間open sets與Y的交集組成。
mko-subspace-topology · definition · v0.10.0
數學敘述
tau_Y={U∩Y:U∈tau_X},重複與空交集正規化。relative-open未必ambient-open且不要求U⊆Y;relative-closed以Y內補集open或F∩Y、F ambient closed判定。全部拓撲公理以Y作相對全集。
代表公式(精確 TeX)
T(Y)
成立條件
- 完整有限X、完整母拓撲與明示subset Y。
- 候選relative sets必為Y的子集。
符號作用域
T— 子空間拓撲Y— 子空間carrier
直觀、定義與常見誤解
每個relative open是O∩Y。
complement在Y內取。
relative與ambient openness不可混同。
要求O⊆Y或把relative-open一律當X中的open。
已採用的推導導讀
相對開集不等於母空間開集原始 MKO 保留;導讀有自己的追加式修訂與驗證界線,不代表新 Lean 證明。
前置知識
驗證界線
complete enumeration只證明宣告有限拓撲。
not_formalized
這不表示內容錯誤;只表示尚未登錄可重播的計算或形式證據。
下一個義務
加入compact subsets與product topology。
同源結構化資料
本頁與互動版共用同一個物件與既有語言 edition;未新增證明或人工審定。
原始 MKO JSON · 純文字 Markdown