有限鏈的基底與全部生成開集

目標與範圍

驗 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 — 基底需覆蓋載體且每個交點有基底內局部細化；生成拓撲是所有子族之聯；既有拓撲的基底還需元素皆開且生成全部開集。

逐步主鏈

B\in\mathcal B

B\subseteq X\quad\text{for all three members}

\bigcup\mathcal B=\{a\}\cup\{a,b\}\cup X

\bigcup\mathcal B=X

B_1,B_2\in\mathcal B

B_1\cap B_2=\min_{\subseteq}(B_1,B_2)\in\mathcal B

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

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

\mathcal T_{\mathcal B}=\{\varnothing,\{a\},\{a,b\},X\}

\mathcal T_{\mathcal B}\text{ is a finite inclusion chain with endpoints}

\mathcal T_{\mathcal B}\text{ is a topology}

\mathcal B\subseteq\tau,\quad\mathcal T_{\mathcal B}=\tau

\mathcal B\text{ is a basis for the supplied }\tau

\mathcal C=\{\{a,b\},\{b,c\}\}

b\in\{a,b\}\cap\{b,c\},\quad\nexists C\in\mathcal C:\ b\in C\subseteq\{b\}

局部子步與引理

本稿無局部子步。

逐步反向審查

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