# 排除全部非平凡開閉集

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

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

derivation-mko-connected-topological-space-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

判斷三點鏈狀拓撲是否連通。

完整有限枚舉；空空間採連通慣例，不使用圖連通。





## 已知條件與符號


- sets
- topology
- definition_here


- G1 — X={a,b,c}，tau={空集,{a},{a,b},X}；連通指不存在非空不交開集對覆蓋 X。


- U,V — 分離候選
- \mathcal F — 全部閉集





## 規則與來源


- mko_definition · cited — 完整有限拓撲上枚舉全部candidate separations/clopen subsets。disconnected需明示witness；connected需排除全部。採空空間connected的vacuous convention，singleton connected。不得混同graph connectivity。 · mko-connected-topological-space
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。
- definition_here · prerequisite — 閉集為開集補集；連通表示沒有兩個非空、不交、聯集為全空間的開集。





## 逐步主鏈

S01 · implies操作前

\varnothing\subset\{a\}\subset\{a,b\}\subset X

操作後

\tau\text{ is a topology}

條件：無

規則：topology · 依賴：G1

葉節點依據：topology

有限鏈的非空聯交各取極端項，空聯與全集也在族中。



S02 · definition操作前

\mathcal F=\{X\setminus U:U\in\tau\}

操作後

\mathcal F=\{X,\{b,c\},\{c\},\varnothing\}

條件：無

規則：definition_here · 依賴：S01

葉節點依據：definition_here

補集枚舉全部閉集。



S03 · equivalent操作前

C\in\tau\cap\mathcal F

操作後

\tau\cap\mathcal F=\{\varnothing,X\}

條件：無

規則：sets · 依賴：S01, S02

葉節點依據：sets

{a} 與 {a,b} 的補集都不開，沒有其他非平凡開閉集。



S04 · implies操作前

X=U\cup V,\ U,V\ne\varnothing,\ U\cap V=\varnothing

操作後

V=X\setminus U

條件：無

規則：sets · 依賴：G1

葉節點依據：sets

若有分離，另一開集必是第一個的補集。



S05 · implies操作前

U,V\in\tau,\quad V=X\setminus U

操作後

U\text{ is nontrivial clopen}

條件：無

規則：sets · 依賴：S04

葉節點依據：sets

分離的兩開集使 U 同時閉，且非空非全。



S06 · implies操作前

\tau\cap\mathcal F=\{\varnothing,X\}

操作後

\text{no separation exists}

條件：無

規則：sets · 依賴：S03, S05

葉節點依據：sets

先前窮盡表排除任何分離所需的非平凡 U。



S07 · definition操作前

\text{no separation of }X

操作後

X\text{ is connected}

條件：無

規則：definition_here · 依賴：S06

葉節點依據：definition_here

套用連通定義；本例其實每個非空開集都含 a，也能排除不交非空對。



S08 · implies操作前

|Y|\le1

操作後

Y\text{ has no two disjoint nonempty parts covering it}

條件：無

規則：sets · 依賴：G1

葉節點依據：sets

空集與單點空間沒有分離，依已宣告慣例皆連通。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1 — 邊界結論不依非空開集含 a 的特例論法。
- S07 · premise_audit · S06 — 補充交集檢查與完整開閉集表一致。
- S06 · premise_audit · S03, S05 — 沒有以未找到一個抽樣分離冒充全部排除。
- S05 · premise_audit · S04 — 這是從分離到開閉集的單向推論。
- S04 · premise_audit · G1 — 不交與覆蓋缺一不可，否則不能推出補集等式。
- S03 · inverse_equivalence · S01, S02 — 四個開集均已對照完整閉集表。
- S02 · premise_audit · S01 — 補集固定相對 X。
- S01 · premise_audit · G1 — 先驗合法拓撲才判連通。





## 錯誤控制與反例

排除需窮盡完整開閉集交表涵蓋全部候選。

空間與圖分離不以頂點或邊的視覺印象判斷拓撲連通。


- {a} 與 {b,c} 是開分離。 → reject — {b,c} 不在拓撲。
- 有三個點所以不連通。 → reject — 連通由拓撲決定，已排除全部分離。
- 圖沒有畫邊，所以此空間不連通。 → reject — 未指定圖，不能替換拓撲定義。





## 結論與限制

本例連通；只有空集與 X 同時開閉。







## 驗證及來源綁定

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


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

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