# 開集與閉集：在四點拓撲中完整分類十六個子集

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

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

derivation-mko-open-closed-set-01 · production-20261019-adopted-96



## 目標與範圍

設 X={1,2,3,4}，τ={∅,{1},{1,2},{3,4},{1,3,4},X}。先驗證 τ 是 X 上的拓撲，再列出全部閉集，並把 X 的十六個子集分成「既開又閉」「只開」「只閉」「既不開也不閉」四類；最後證明在任何拓撲空間中 ∅ 與 X 都既開又閉，以及兩個閉集的聯集仍是閉集。

在 MKO 範圍內工作：底集合 X 與拓撲 τ 固定（假設 a1），所有補集都相對同一個 X（假設 a2）。一般性結論只證明「∅ 與 X 永遠既開又閉」與「兩個閉集的聯集是閉集」；任意多個閉集之交的對偶敘述只說明不另證。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- set_operations_def
- set_extensionality
- subset_def
- finite_counting_basics
- nat_induction


- G1 — 底集合 X={1,2,3,4}（MKO 假設 a1）。
- G2 — 子集合族 τ={∅,{1},{1,2},{3,4},{1,3,4},X}，每個成員都是 X 的子集合。
- G3 — 所有補集都取相對於 X 的補集 X∖C，候選集合都先確認是 X 的子集合（MKO 假設 a2）。


- X — 底集合 {1,2,3,4}
- \tau — X 上的拓撲（開集族）
- \mathcal{C} — 閉集族 {C⊆X ∣ X∖C∈τ}
- X\setminus C — C 相對於 X 的補集
- \mathcal{P}(X) — X 的全部子集





## 規則與來源


- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- topology_def · prerequisite — 拓撲：X 上的開集族 τ 包含 ∅ 與 X，對任意聯集與有限交集封閉。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- mko_open_closed_def · cited — 給定拓撲空間 (X,τ)，U⊆X 稱為開集當且僅當 U∈τ；C⊆X 稱為閉集當且僅當 X∖C∈τ。開與閉不是互斥分類，∅ 與 X 永遠同時開且閉。 · mko-open-closed-set
- mko_topological_space_def · cited — X 上的拓撲是子集合族 τ⊆P(X)，滿足 ∅∈τ、X∈τ、τ 中任意子族的聯集仍在 τ，且 τ 中任意有限子族的交集仍在 τ；空族的聯集是 ∅，空族的交集按 X 解讀。 · mko-topological-space
- L_finite_family · lemma — 設 τ 是 X 的有限子集合族。若 ∅∈τ 且 τ 對兩個成員的聯集封閉，則 τ 的每個子族的聯集都在 τ；若 X∈τ 且 τ 對兩個成員的交集封閉，則 τ 的每個子族的交集（空族的交集為 X）都在 τ。
- L_double_complement · lemma — 對每個 C⊆X，X∖(X∖C)=C。
- L_demorgan · lemma — 對 A,B⊆X，X∖(A∪B)=(X∖A)∩(X∖B)。





## 逐步主鏈

S01 · theorem_application操作前

\tau=\{\varnothing,\{1\},\{1,2\},\{3,4\},\{1,3,4\},X\}

操作後

(X,\tau)\ \text{is a topological space}

條件：\tau\ \text{finite}; \varnothing,X\in\tau

規則：L_finite_family · 依賴：G1, G2

葉節點依據：topology_def + set_operations_def + nat_induction

τ 的六個成員都是 X 的子集合，且 ∅∈τ、X∈τ。τ 是有限族，依引理 L_finite_family（在 S01.1、S01.2 證明），只要檢查任兩個成員的聯集與交集都在 τ，就得到對每個子族的聯集與每個有限子族的交集都封閉；這個兩兩檢查在 S01.3 完成。所以 (X,τ) 是拓撲空間，之後才能談開與閉。



S02 · equivalent操作前

C\subseteq X\ \text{closed}\iff X\setminus C\in\tau

操作後

C\ \text{closed}\iff C=X\setminus U\ \text{for some}\ U\in\tau

條件：C\subseteq X

規則：L_double_complement · 依賴：S01, G3

葉節點依據：def_unfold + set_operations_def + set_extensionality

依 MKO 定義，C 是閉集當且僅當 X∖C∈τ。(⇒) 令 U=X∖C∈τ，依 L_double_complement 得 C=X∖(X∖C)=X∖U。(⇐) 若 C=X∖U 且 U∈τ，則 X∖C=X∖(X∖U)=U∈τ。所以閉集恰好是開集的補集，閉集族可由逐一取補集算出。



S03 · implies操作前

\{X\setminus U\mid U\in\tau\}

操作後

\mathcal{C}=\{X,\{2,3,4\},\{3,4\},\{1,2\},\{2\},\varnothing\}

條件：無

規則：set_operations_def · 依賴：S02, G2

葉節點依據：set_operations_def + injective_surjective_def

逐一取補集：X∖∅=X，X∖{1}={2,3,4}，X∖{1,2}={3,4}，X∖{3,4}={1,2}，X∖{1,3,4}={2}，X∖X=∅。依 S02，這六個集合就是全部閉集。因為取補集可由自身逆回（L_double_complement），不同開集給出不同閉集，所以恰有 6 個閉集。



S04 · implies操作前

\tau,\ \mathcal{C}

操作後

\tau\cap\mathcal{C}=\{\varnothing,\{1,2\},\{3,4\},X\}

條件：無

規則：set_operations_def · 依賴：G2, S03

葉節點依據：set_operations_def

比對兩張表，同時出現在 τ 與 𝒞 中的是 ∅、{1,2}、{3,4}、X，這四個集合既開又閉。除了必然的 ∅ 與 X，{1,2} 與 {3,4} 也是 clopen：它們互為補集，而且都是開集。



S05 · implies操作前

\tau,\ \mathcal{C}

操作後

\tau\setminus\mathcal{C}=\{\{1\},\{1,3,4\}\}

條件：無

規則：set_operations_def · 依賴：G2, S03

葉節點依據：set_operations_def + mko_open_closed_def

在 τ 中但不在 𝒞 中的是 {1} 與 {1,3,4}：它們是開集，但補集 {2,3,4} 與 {2} 不在 τ，所以不是閉集。



S06 · implies操作前

\tau,\ \mathcal{C}

操作後

\mathcal{C}\setminus\tau=\{\{2\},\{2,3,4\}\}

條件：無

規則：set_operations_def · 依賴：G2, S03

葉節點依據：set_operations_def + mko_open_closed_def

在 𝒞 中但不在 τ 中的是 {2} 與 {2,3,4}：它們是閉集，但不是開集。



S07 · implies操作前

|\mathcal{P}(X)|=2^4=16,\ |\tau\cup\mathcal{C}|=6+6-4=8

操作後

\mathcal{P}(X)\setminus(\tau\cup\mathcal{C})=\{\{3\},\{4\},\{1,3\},\{1,4\},\{2,3\},\{2,4\},\{1,2,3\},\{1,2,4\}\}

條件：無

規則：finite_counting_basics · 依賴：S04, S05, S06

葉節點依據：finite_counting_basics + numeric_evaluation + set_operations_def

X 有 2^4=16 個子集。τ∪𝒞 有 6+6−4=8 個成員（重疊的是 S04 的 4 個 clopen 集），所以恰有 16−8=8 個子集既不開也不閉，列出如上。核對：4 個 clopen、2 個只開、2 個只閉、8 個兩者皆非，合計 16。子步 S07.1 以 {3} 為例逐項核對。



S08 · implies操作前

(Y,\sigma)\ \text{any topological space}

操作後

\varnothing\ \text{and}\ Y\ \text{are clopen in}\ (Y,\sigma)

條件：無

規則：forall_intro · 依賴：mko_topological_space_def, mko_open_closed_def

葉節點依據：forall_intro + set_operations_def + mko_topological_space_def

取任意拓撲空間 (Y,σ)。依拓撲定義 ∅∈σ、Y∈σ，所以兩者都是開集。又 Y∖∅=Y∈σ，故 ∅ 是閉集；Y∖Y=∅∈σ，故 Y 是閉集。證明沒有用到 Y 或 σ 的任何特殊性質，依全稱推廣對所有拓撲空間成立；本例中即 S04 的 ∅ 與 X。



S09 · theorem_application操作前

C_1,C_2\in\mathcal{C}

操作後

X\setminus(C_1\cup C_2)=(X\setminus C_1)\cap(X\setminus C_2)\in\tau,\ \text{so}\ C_1\cup C_2\in\mathcal{C}

條件：C_1,C_2\subseteq X

規則：L_demorgan · 依賴：S01, S02

葉節點依據：set_operations_def + de_morgan_logic + topology_def

設 C1、C2 是閉集，即 X∖C1、X∖C2∈τ。依 De Morgan 引理 L_demorgan（在 S09.1、S09.2 證明），X∖(C1∪C2)=(X∖C1)∩(X∖C2)，這是兩個開集的交集，依拓撲定義仍在 τ。所以 C1∪C2 是閉集。這個論證適用於任何拓撲空間，再對個數歸納可推廣到有限多個閉集。



S10 · implies操作前

\{2\},\ \{3,4\}\in\mathcal{C}

操作後

\{2\}\cup\{3,4\}=\{2,3,4\}\in\mathcal{C},\quad X\setminus\{2,3,4\}=\{1\}=\{1,3,4\}\cap\{1,2\}

條件：無

規則：forall_elim · 依賴：S09, S03

葉節點依據：forall_elim + set_operations_def

把 S09 用在 C1={2}、C2={3,4}：聯集 {2,3,4} 應是閉集。直接核對：X∖{2,3,4}={1}∈τ；而依 De Morgan，它也等於 (X∖{2})∩(X∖{3,4})={1,3,4}∩{1,2}={1}。兩種算法一致。



S11 · implies操作前

\text{claim:}\ C\ \text{closed}\iff C\notin\tau

操作後

\{1,2\}\in\tau\cap\mathcal{C},\ \{3\}\notin\tau\cup\mathcal{C}\ \Rightarrow\ \text{claim false in both directions}

條件：無

規則：quantifier_negation · 依賴：S04, S07.1

葉節點依據：quantifier_negation + iff_intro

檢驗 MKO 指出的誤解「閉就是不開」。(⇒) 方向的反例：{1,2} 是閉集，卻也是開集。(⇐) 方向的反例：{3} 不是開集，卻也不是閉集（S07.1）。兩個方向都有反例，所以開與閉是兩個獨立的性質，四類都可能出現。







## 局部子步與引理

S01.1 · induction_step操作前

F\subseteq\tau,\ |F|=k

操作後

\textstyle\bigcup F\in\tau\ \text{for every}\ k

條件：\varnothing\in\tau; U,V\in\tau\Rightarrow U\cup V\in\tau

規則：nat_induction · 依賴：nat_induction, set_operations_def, finite_counting_basics

葉節點依據：nat_induction + set_operations_def + finite_counting_basics

τ 有限，所以每個子族 F 都有限，對其成員數 k 歸納。k=0：空族的聯集是 ∅，而 ∅∈τ。k→k+1：取 F 的一個成員 U，令 F′=F∖{U}，則 |F′|=k，∪F=(∪F′)∪U；依歸納假設 ∪F′∈τ，再依兩兩聯集封閉得 ∪F∈τ。這證得引理的聯集部分。



S01.2 · induction_step操作前

F\subseteq\tau,\ |F|=k

操作後

\textstyle\bigcap F\in\tau\ \text{for every}\ k\ (\bigcap\varnothing=X)

條件：X\in\tau; U,V\in\tau\Rightarrow U\cap V\in\tau

規則：nat_induction · 依賴：nat_induction, set_operations_def, finite_counting_basics

葉節點依據：nat_induction + set_operations_def

同樣對 k 歸納。k=0：空族的交集按 X 解讀，X∈τ。k→k+1：∩F=(∩F′)∩U，依歸納假設與兩兩交集封閉得 ∩F∈τ。S01.1 與 S01.2 合起來證得 L_finite_family。



S01.3 · implies操作前

U,V\in\tau

操作後

U\cup V\in\tau,\ U\cap V\in\tau

條件：無

規則：set_operations_def · 依賴：G2

葉節點依據：set_operations_def + finite_counting_basics

含 ∅ 或 X 的組合都直接回到 τ（∅∪A=A、∅∩A=∅、X∪A=X、X∩A=A）。其餘六組：{1}∪{1,2}={1,2}、交集 {1}；{1}∪{3,4}={1,3,4}、交集 ∅；{1}∪{1,3,4}={1,3,4}、交集 {1}；{1,2}∪{3,4}=X、交集 ∅；{1,2}∪{1,3,4}=X、交集 {1}；{3,4}∪{1,3,4}={1,3,4}、交集 {3,4}。每個結果都在 τ 中。



S02.1 · equivalent操作前

x\in X\setminus(X\setminus C)

操作後

x\in C

條件：C\subseteq X

規則：set_operations_def · 依賴：set_operations_def, set_extensionality

葉節點依據：set_operations_def + de_morgan_logic + set_extensionality

x∈X∖(X∖C) ⇔ x∈X 且不是（x∈X 且 x∉C）⇔ x∈X 且 x∈C ⇔ x∈C；最後一步用到 C⊆X。依集合外延性，X∖(X∖C)=C，證得 L_double_complement。



S07.1 · implies操作前

\{3\}

操作後

\{3\}\notin\tau,\ X\setminus\{3\}=\{1,2,4\}\notin\tau

條件：無

規則：mko_open_closed_def · 依賴：G2, S03

葉節點依據：mko_open_closed_def + set_operations_def

{3} 不在 τ 的六個成員中，所以不是開集；它的補集 {1,2,4} 也不在 τ，所以 {3} 不是閉集。{3} 既不開也不閉，這直接否定「不開就是閉」。



S09.1 · implies操作前

x\in X\setminus(A\cup B)

操作後

x\in(X\setminus A)\cap(X\setminus B)

條件：無

規則：set_operations_def · 依賴：set_operations_def, de_morgan_logic

葉節點依據：set_operations_def + de_morgan_logic

(⊆) x∈X∖(A∪B) 表示 x∈X 且不是（x∈A 或 x∈B）；依邏輯 De Morgan，等於 x∈X、x∉A 且 x∉B，所以 x∈X∖A 且 x∈X∖B。



S09.2 · implies操作前

x\in(X\setminus A)\cap(X\setminus B)

操作後

x\in X\setminus(A\cup B);\ \text{hence}\ X\setminus(A\cup B)=(X\setminus A)\cap(X\setminus B)

條件：無

規則：set_extensionality · 依賴：S09.1, set_extensionality

葉節點依據：set_operations_def + set_extensionality

(⊇) 若 x∈X、x∉A 且 x∉B，則 x 不在 A∪B，所以 x∈X∖(A∪B)。兩個包含合起來，依集合外延性得等式，證得 L_demorgan。







## 逐步反向審查


- S11 · premise_audit · S04, S07.1, quantifier_negation — 此處要分別否定兩個方向，所以每個方向各給一個反例，兩者都由前面的具體計算提供；若只需否定整個全稱等價，任一方向的一個反例已足夠。
- S10 · premise_audit · S09, S03, forall_elim — 這是一般結論的一個實例與交叉核對，不能反過來證明一般結論。
- S09.2 · premise_audit · S09.1, set_extensionality, set_operations_def — 集合等式需要兩個方向的包含，都已證明。
- S09.1 · premise_audit · set_operations_def, de_morgan_logic — 此子步只證一個包含方向；另一方向在 S09.2。
- S09 · premise_audit · L_demorgan, mko_topological_space_def, mko_open_closed_def — 需要有限交集封閉；對無限多個閉集的聯集不宣稱成立（一般拓撲中可能不閉）。
- S08 · premise_audit · mko_topological_space_def, mko_open_closed_def, forall_intro — 只用到兩條拓撲公理與閉集定義；不宣稱其他集合也一定 clopen（例如 {1} 不是）。
- S07.1 · premise_audit · G2, mko_open_closed_def — 兩個判定都只用定義與 τ 的完整列表；補集在 X 中計算。
- S07 · premise_audit · S04, S05, S06, finite_counting_basics — 計數用到聯集的容斥（N2、N3、N4 可重算）。列出的八個集合都不在兩張表中，與計數一致。
- S06 · premise_audit · S03, G2 — 「不是開集」由與 τ 的六個成員逐一比對得到。
- S05 · premise_audit · S03, set_operations_def — 每個「不是閉集」都由補集不在 τ 這個具體檢查支持。
- S04 · premise_audit · G2, S03, set_operations_def — 交集需要兩張完整列表；結論是集合族的等式。
- S03 · premise_audit · S02, set_operations_def, L_double_complement — 需要 S02 的等價與 τ 的完整列表；每個補集都在 X 內計算。
- S02.1 · inverse_equivalence · set_operations_def, set_extensionality, de_morgan_logic — 每一步都是邏輯等價（De Morgan 與 x∈X 已知），所以雙向成立。若 C 不是 X 的子集，最後一步只得 x∈C∩X，公式失效。
- S02 · inverse_equivalence · L_double_complement, mko_open_closed_def — 兩個方向都已寫出理由，都只用到雙重補集與定義。補集必須相對同一個 X，否則雙重補集公式不成立。
- S01.3 · premise_audit · G2, set_operations_def — 四個非平凡成員兩兩配對共有 comb(4,2)=6 組，全部列出（N1），沒有遺漏。
- S01.2 · premise_audit · nat_induction, set_operations_def — 需要 X∈τ 作為空族交集的基底，與兩兩交集封閉。
- S01.1 · premise_audit · nat_induction, set_operations_def, finite_counting_basics — 歸納需要每個子族都有有限個成員，這來自 τ 有限。基底需要 ∅∈τ，不能省略空族。
- S01 · premise_audit · G2, L_finite_family, mko_topological_space_def — 需要 τ 有限、含 ∅ 與 X、以及 S01.3 的兩兩檢查。引理只在有限族時成立；無限族只對兩兩聯集封閉並不足夠（見錯誤控制三）。





## 錯誤控制與反例

閉不是「不開」MKO 指出的誤解是把 closed 讀成 not open。本例中 {1,2} 同時開且閉，{3} 兩者皆非（S11）。判定閉集只能用定義：補集是否在 τ 中。

補集要相對同一個 X若把 {1,2} 的補集錯算在 {1,2,3} 中，會得到 {3}∉τ 而誤判 {1,2} 不閉；正確的 X∖{1,2}={3,4}∈τ。若在 {1,2,3,4,5} 中取 {3,4} 的補集，得到 {1,2,5}，它甚至不是 X 的子集，與 τ 的比對失去意義（MKO 假設 a2）。

兩兩封閉只在有限族時足夠S01 能只檢查兩兩聯集，是因為 τ 有限（L_finite_family）。反例：ℕ 的全部有限子集再加上 ℕ 本身，這個族含 ∅ 與 ℕ，對兩兩聯集與交集封閉，但所有 {2k} 的聯集是偶數集，它無限且不等於 ℕ，不在族中，所以不是拓撲。


- {3} 不是開集，所以 {3} 是閉集 → reject — X∖{3}={1,2,4}∉τ，所以 {3} 不是閉集；它既不開也不閉。
- {1,2} 是閉集，所以它不是開集 → reject — {1,2}∈τ，它同時開且閉。
- 在 {1,2,3,4,5} 中 {3,4} 的補集是 {1,2,5}∉τ，所以 {3,4} 不是閉集 → reject — 補集必須相對 X：X∖{3,4}={1,2}∈τ，{3,4} 是閉集。
- 閉集恰好是不在 τ 中的 10 個子集 → reject — 閉集只有 6 個（S03），其中 4 個也在 τ 中；不在 τ 中的 10 個子集裡有 8 個不是閉集。





## 結論與限制

τ 是 X={1,2,3,4} 上的拓撲；閉集族為 {X,{2,3,4},{3,4},{1,2},{2},∅}。十六個子集分為：既開又閉 ∅、{1,2}、{3,4}、X；只開 {1}、{1,3,4}；只閉 {2}、{2,3,4}；其餘八個既不開也不閉。一般地，∅ 與 X 在任何拓撲空間中都既開又閉，兩個閉集的聯集仍是閉集。


- MKO 第二段的對偶敘述「任意多個閉集之交仍閉」可由任意族的 De Morgan 定律推得；本稿只證明兩個閉集之聯集的情形，任意族情形未另寫子步。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: db4ff6acc8064d0f256eceeebb39a241b3986504cee1fd23ae8da1de54588f78
- original source SHA-256: db4ff6acc8064d0f256eceeebb39a241b3986504cee1fd23ae8da1de54588f78
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-open-closed-set-01.json)