# 有限鏈的基底與全部生成開集 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-topological-basis/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-topological-basis-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 驗 B={{a},{a,b},X} 是指定拓撲的基底。 完整有限基底與拓撲；不混同子基底。 ## 已知條件與符號 - sets - topology - definition_here - G1 — X={a,b,c}，B={{a},{a,b},X}；目標 tau={空集,{a},{a,b},X}。 - \mathcal B — 基底候選 - \mathcal T_{\mathcal B} — 全部基底聯 ## 規則與來源 - mko_definition · cited — 每個basis element是X的子集且全部聯集覆蓋X；對x∈B1∩B2，存在B3使x∈B3⊆B1∩B2。若聲稱為既有拓撲的basis，還需basis elements皆開且每個open set為basis聯集。basis不可與subbasis混同。 · mko-topological-basis - sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。 - topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。 - definition_here · prerequisite — 基底需覆蓋載體且每個交點有基底內局部細化；生成拓撲是所有子族之聯；既有拓撲的基底還需元素皆開且生成全部開集。 ## 逐步主鏈 S01 · implies操作前 B\in\mathcal B 操作後 B\subseteq X\quad\text{for all three members} 條件：無 規則：sets · 依賴：G1 葉節點依據：sets 三個基底候選均在同一載體內。 S02 · implies操作前 \bigcup\mathcal B=\{a\}\cup\{a,b\}\cup X 操作後 \bigcup\mathcal B=X 條件：無 規則：sets · 依賴：G1, S01 葉節點依據：sets 因 X 自身列在基底中，覆蓋條件成立。 S03 · implies操作前 B_1,B_2\in\mathcal B 操作後 B_1\cap B_2=\min_{\subseteq}(B_1,B_2)\in\mathcal B 條件：無 規則：sets · 依賴：G1 葉節點依據：sets 三個集合是包含鏈，六種無序可重複配對的交分別是較小那項。 S04 · implies操作前 x\in B_1\cap B_2 操作後 B_3=B_1\cap B_2,\quad x\in B_3\subseteq B_1\cap B_2 條件：無 規則：sets · 依賴：S03 葉節點依據：sets 取交集本身作局部細化，因前一步已證它仍在基底。 S05 · definition操作前 \mathcal T_{\mathcal B}=\{\bigcup\mathcal C:\mathcal C\subseteq\mathcal B\} 操作後 \mathcal T_{\mathcal B}=\{\varnothing,\{a\},\{a,b\},X\} 條件：無 規則：definition_here · 依賴：G1 葉節點依據：definition_here 八個子族的聯只有四個不同結果；空子族給空集，非空子族取最大項。 S06 · implies操作前 \mathcal T_{\mathcal B}\text{ is a finite inclusion chain with endpoints} 操作後 \mathcal T_{\mathcal B}\text{ is a topology} 條件：無 規則：topology · 依賴：S05 葉節點依據：topology 完整四項族的聯交封閉性由鏈性得到。 S07 · definition操作前 \mathcal B\subseteq\tau,\quad\mathcal T_{\mathcal B}=\tau 操作後 \mathcal B\text{ is a basis for the supplied }\tau 條件：無 規則：definition_here · 依賴：G1, S05 葉節點依據：definition_here 每個基底元素開且每個目標開集是基底聯，雙向生成責任都成立。 S08 · implies操作前 \mathcal C=\{\{a,b\},\{b,c\}\} 操作後 b\in\{a,b\}\cap\{b,c\},\quad\nexists C\in\mathcal C:\ b\in C\subseteq\{b\} 條件：無 規則：sets · 依賴：G1 葉節點依據：sets 一個覆蓋 X 的族也可能沒有交細化，展示覆蓋不等於基底。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1 — 失敗點 b 與全部兩個候選都明示，可窮盡拒絕。 - S07 · premise_audit · G1, S05 — 只核基底元素開仍不足，S05 提供反向生成。 - S06 · premise_audit · S05 — 目標族不是先被假定為拓撲，而是已核公理。 - S05 · premise_audit · G1 — 列舉了全部聯而不是只列基底元素。 - S04 · premise_audit · S03 — 不是要求所有基底一般都對交封閉；此例特別可直接取交。 - S03 · premise_audit · G1 — 鏈論法涵蓋全部配對，沒有未核例外。 - S02 · premise_audit · G1, S01 — 覆蓋只是第一條基底公理，尚須交細化。 - S01 · premise_audit · G1 — 不允許基底元素含載體以外的點。 ## 錯誤控制與反例 交點量詞每對及交內每點都須有細化，不能只核覆蓋。 雙向生成核基底皆開，並核全部目標開集可生成。 - 任何覆蓋都是基底。 → reject — S08 的兩集合覆蓋卻在 b 無交細化。 - 生成拓撲不必包含空集。 → reject — 空聯必須列入。 - 基底元素開已足夠證它生成既有拓撲。 → reject — 還要每個既有開集都是它們的聯。 ## 結論與限制 B 是指定 tau 的基底，生成恰好四個開集。 ## 驗證及來源綁定 0 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 16ceb5eebc9f37a1b5a839cd909ba4c61c0319da66fca248b310dbd7dd5c0c8c - original source SHA-256: 16ceb5eebc9f37a1b5a839cd909ba4c61c0319da66fca248b310dbd7dd5c0c8c - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-topological-basis-01.json)