拓撲空間：完整驗證三點集合上的一個鏈狀開集族，並辨認非拓撲

目標與範圍

設 X={a,b,c}（a、b、c 相異）。(1) 證明 τ₁={∅,{a},{a,b},X} 是 X 上的拓撲，涵蓋全部 16 個子族（含空族）；(2) 證明 τ₂={∅,{a},{b},X} 不是拓撲，並指出它通過了哪些檢查；(3) 比較 τ₁ 與不可分拓撲、離散拓撲的粗細；(4) 在 ℕ 上，證明 τ_fin={ℕ 的有限子集}∪{ℕ} 對兩兩聯集與有限交集封閉，卻不是拓撲。

依 MKO 的定義（含空族約定 a2）逐條驗證。有限例以「鏈」引理一次處理所有非空子族，再計數確認 16 個子族全部涵蓋，不是抽查。無窮例只用來說明「兩兩封閉」與「任意封閉」的差別。不處理連續映射、基或度量拓撲；不改動 canonical MKO 或英文 edition。

已知條件與符號

• subset_def
• set_operations_def
• set_extensionality
• nat_induction
• numeric_evaluation

• G1 — X={a,b,c}，a、b、c 兩兩相異；τ₁={∅,{a},{a,b},X}；τ₂={∅,{a},{b},X}。
• G2 — MKO 假設 a2：任意聯集包含空族情形，有限交包含空族情形；空族的交集按 X 解讀。
• G3 — ℕ 包含 0；τ_fin={A⊆ℕ : A 有限}∪{ℕ}。

• X=\{a,b,c\} — 底集合，a、b、c 相異
• \tau_1,\ \tau_2 — 兩個候選子集合族
• \mathcal{S}\subseteq\tau — τ 的子族
• \bigcup\mathcal{S},\ \bigcap\mathcal{S} — 子族的聯集與交集（交集相對於 X）
• \mathcal{P}(X) — 冪集，即離散拓撲
• \tau_{\mathrm{fin}} — ℕ 上的候選族
• E — ℕ 中偶數的集合

規則與來源

• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• 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，即兩者有相同元素。
• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• mko_topology_def · cited — 給定集合 X，X 上的拓撲是子集合族 τ⊆P(X)，滿足 ∅∈τ、X∈τ、τ 中任意子族的聯集仍在 τ，且 τ 中任意有限子族的交集仍在 τ；(X,τ) 稱為拓撲空間。 · mko-topological-space
• family_ops · prerequisite — 對 X 的子集合族 𝒮：x∈⋃𝒮 ⇔ 存在 A∈𝒮 使 x∈A；x∈⋂𝒮 ⇔ x∈X 且對每個 A∈𝒮 都有 x∈A。因此 ⋃∅=∅、⋂∅=X。
• finite_sets · prerequisite — 兩個有限集合的聯集有限；有限集合的子集合有限；ℕ 的每個有限非空子集都有最大元素。
• L_chain_extremes · lemma — 若有限非空集合族 𝒮 中任兩成員都可用 ⊆ 比較，則 𝒮 有最大成員 M（每個 A∈𝒮 有 A⊆M）與最小成員 m（每個 A∈𝒮 有 m⊆A）。
• L_chain_union · lemma — 若 M∈𝒮 是 𝒮 的最大成員，則 ⋃𝒮=M；若 m∈𝒮 是最小成員，則 ⋂𝒮=m（𝒮 的成員都是 X 的子集）。

逐步主鏈

\tau\ \text{is a topology on}\ X

\tau\subseteq\mathcal{P}(X),\ \varnothing,X\in\tau,\ \forall\mathcal{S}\subseteq\tau:\ \bigcup\mathcal{S}\in\tau,\ \forall\ \text{finite}\ \mathcal{S}\subseteq\tau:\ \bigcap\mathcal{S}\in\tau

\tau_1=\{\varnothing,\{a\},\{a,b\},X\}

\tau_1\subseteq\mathcal{P}(X)

\mathcal{S}=\varnothing\subseteq\tau_1

\bigcup\varnothing=\varnothing\in\tau_1,\quad \bigcap\varnothing=X\in\tau_1

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

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

\varnothing\neq\mathcal{S}\subseteq\tau_1

\mathcal{S}\ \text{has a largest member}\ M\ \text{and a smallest member}\ m

M,\ m\ \text{largest and smallest in}\ \mathcal{S}

\bigcup\mathcal{S}=M,\quad \bigcap\mathcal{S}=m

\mathcal{S}\subseteq\tau_1\ \text{arbitrary}

\bigcup\mathcal{S}\in\tau_1

\mathcal{S}\subseteq\tau_1\ \text{finite}

\bigcap\mathcal{S}\in\tau_1

\tau_1\subseteq\mathcal{P}(X),\ \text{unions and finite intersections closed}

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

\{a\},\ \{b\}\in\tau_2

\{a\}\cup\{b\}=\{a,b\}\notin\tau_2

\tau_2=\{\varnothing,\{a\},\{b\},X\}

\varnothing,X\in\tau_2,\ \text{and}\ A\cap B\in\tau_2\ \text{for all}\ A,B\in\tau_2

\{\varnothing,X\},\ \tau_1,\ \mathcal{P}(X)

\{\varnothing,X\}\subsetneq\tau_1\subsetneq\mathcal{P}(X)

A,B\in\tau_{\mathrm{fin}}

A\cup B\in\tau_{\mathrm{fin}},\ A\cap B\in\tau_{\mathrm{fin}};\ \varnothing,\mathbb{N}\in\tau_{\mathrm{fin}}

\mathcal{S}=\{\{2k\}:k\in\mathbb{N}\}\subseteq\tau_{\mathrm{fin}}

\bigcup\mathcal{S}=E\notin\tau_{\mathrm{fin}}

\text{goals (1) to (4)}

\tau_1\ \text{topology};\ \tau_2,\ \tau_{\mathrm{fin}}\ \text{not topologies};\ \{\varnothing,X\}\subsetneq\tau_1\subsetneq\mathcal{P}(X)

局部子步與引理

|\mathcal{S}|=1,\ \mathcal{S}=\{A\}

M=m=A

|\mathcal{S}|=n+1,\ \mathcal{S}=\mathcal{S}'\cup\{A\},\ \mathcal{S}'\ \text{has}\ M',m'

\mathcal{S}\ \text{has a largest and a smallest member}

P(1)\ \land\ \forall n\ge 1\,(P(n)\Rightarrow P(n+1))

\forall n\ge 1:\ P(n)

M\in\mathcal{S},\ \forall A\in\mathcal{S}:\ A\subseteq M

\bigcup\mathcal{S}=M

m\in\mathcal{S},\ \forall A\in\mathcal{S}:\ m\subseteq A,\ m\subseteq X

\bigcap\mathcal{S}=m

1\in E\ ?

1\notin E,\ \text{so}\ E\neq\mathbb{N}

E\ \text{finite}\ ?

E\ \text{is infinite}

逐步反向審查

• S15 · sufficient_goal_reduction · S09, S10, S12, S14, and_intro_elim — 目標 G：四個小題。足夠條件 H：S09、S10、S12、S14 的結論；H⇒G 只是合取，H 由已知正向證成。
• S14.2 · premise_audit · finite_sets, contradiction — 矛盾依賴「有限非空自然數集合有最大元素」與 2j+2=2(j+1)（N6）。
• S14.1 · premise_audit · set_extensionality, order_basics — 一個不屬於 E 的自然數就足以說明兩集合不等（N5）。
• S14 · premise_audit · G3, family_ops — 反例需要一個無窮子族；有限子族的聯集不會出現這個問題（S13）。結論依賴 S14.1、S14.2。
• S13 · premise_audit · G3, finite_sets, case_analysis — 情況窮盡；只宣稱兩兩（因而有限）封閉，不宣稱任意聯集封閉。
• S12 · premise_audit · S09, subset_def, set_operations_def — 粗細比較的是開集族的包含（MKO 段落 2），不是底集合的大小；兩個嚴格包含各由一個見證成員（{a} 與 {b}）確認。
• S11 · premise_audit · G1, set_operations_def — 這一步不改變 S10 的結論，只說明 τ₂ 通過了哪些檢查。
• S10 · premise_audit · G1, set_operations_def, set_extensionality — 一個反例子族就足以否定；這用到 a、b、c 兩兩相異（G1）。
• S09 · sufficient_goal_reduction · S02, S03, S07, S08, mko_topology_def, and_intro_elim — 目標 G：τ₁ 是拓撲。足夠條件 H：S02、S03、S07、S08 同時成立；H⇒G 由定義。H 由 G1、G2 正向證成，沒有把 G 當作前提。
• S08 · premise_audit · S03, S05, S06, case_analysis — 兩種情況窮盡所有有限子族。
• S07 · premise_audit · S03, S05, S06, case_analysis — 「空」與「非空」窮盡所有子族；τ₁ 有限，所以「任意子族」都是有限子族，沒有遺漏無窮子族。
• S06.2 · premise_audit · family_ops, set_extensionality — 用到 m 最小與 m⊆X；沒有使用引理本身。
• S06.1 · premise_audit · family_ops, set_extensionality — 兩個包含各自用到 M∈𝒮 與 M 最大；沒有使用引理本身。
• S06 · premise_audit · S05, L_chain_union — 需要 M、m 屬於 𝒮；空族沒有最大成員，所以空族已在 S03 單獨處理。
• S05.3 · premise_audit · S05.1, S05.2, nat_induction — 基礎與歸納步都已證，沒有使用引理本身。
• S05.2 · premise_audit · subset_def, case_analysis — 兩種情況由可比較性窮盡；只用到 ⊆ 的遞移性與歸納假設。
• S05.1 · premise_audit · subset_def — 只用 ⊆ 的自反性。
• S05 · premise_audit · S04, L_chain_extremes — 引理需要有限、非空、可比較三個前提，都已確認。
• S04 · premise_audit · G1, subset_def — 只宣稱這四個集合成鏈；一般的集合族不必成鏈（τ₂ 中 {a} 與 {b} 不可比較）。
• S03 · premise_audit · G2, family_ops — 交集取 X 是相對於固定底集合的約定（MKO 假設 a2）；沒有這個約定，⋂∅ 沒有意義。
• S02 · premise_audit · G1, subset_def — 逐一檢查四個成員；不宣稱其他條件。
• S01 · premise_audit · G1, G2, mko_topology_def — 此步只展開定義；任何一個條件失敗就不是拓撲。

錯誤控制與反例

不是任何子集合族都是拓撲

MKO 指出的誤解：把任何子集合族當成拓撲。τ₂ 含 ∅ 與 X，也對交集封閉，卻因 {a}∪{b}={a,b}∉τ₂ 而不是拓撲（S10、S11）。必須逐類檢查全部條件。

兩兩封閉不等於任意封閉

MKO 指出的另一個誤解：把只對兩兩聯集封閉當成對任意聯集封閉。τ_fin 對兩兩聯集封閉（S13），但無窮多個單點集 {0}、{2}、{4} 等的聯集是偶數集合，不在 τ_fin 中（S14）。在含 ∅ 的有限族上，每個子族都有限，二元聯集封閉再加空聯集條件即可涵蓋任意聯集；若未含 ∅，空子族仍可能使它失敗；本稿對 τ₁ 改用鏈引理一次處理全部子族。

別漏掉空族

公理 ∅∈τ、X∈τ 正是空族聯集與空族交集的情形（S03）。漏掉 ∅ 的 {{a},{a,b},X} 或漏掉 X 的 {∅,{a},{a,b}} 都不是拓撲。

粗細比較的是開集族

τ₁⊆P(X) 表示 P(X) 較細、τ₁ 較粗；這是開集族的包含關係，與底集合 X 的大小無關（MKO 段落 2）。

• τ₂={∅,{a},{b},X} 含 ∅、X 且對交集封閉，所以是拓撲 → reject — {a}∪{b}={a,b}∉τ₂，聯集條件失敗。
• τ_fin 對兩兩聯集封閉，所以對任意聯集封閉，是 ℕ 上的拓撲 → reject — 單點集 {2k} 的聯集是偶數集合，既非有限也不等於 ℕ。
• {{a},{a,b},X} 是 X 上的拓撲 → reject — 缺少 ∅，也就是空索引族的聯集不在族中；僅缺少 ∅ 這一點，就足以否定它是拓撲。
• {∅,{a},{a,b}} 是 X 上的拓撲 → reject — 缺少 X，也就是空族的交集（按 X 解讀）不在族中。
• τ₁ 比 P(X) 細 → reject — τ₁⊊P(X)，所以 P(X) 較細；例如 {b}∈P(X) 但 {b}∉τ₁。

結論與限制

τ₁={∅,{a},{a,b},X} 是 X={a,b,c} 上的拓撲：它是一條鏈，非空子族的聯集與交集分別是最大與最小成員，空族給出 ∅ 與 X，16 個子族全部涵蓋。τ₂={∅,{a},{b},X} 不是拓撲，因 {a}∪{b}={a,b}∉τ₂，雖然它含 ∅、X 且對交集封閉。{∅,X}⊊τ₁⊊P(X)。ℕ 上的 τ_fin 對兩兩聯集與有限交集封閉，但偶數集合是其單點集的聯集且不在 τ_fin 中，所以不是拓撲。

• finite_sets（兩有限集合之聯集有限、有限集之子集有限、有限非空自然數集有最大元素）作為前置知識使用，未在本稿證明。
• 一般敘述須補上空族條件：有限集合族若含 ∅ 且對二元聯集封閉，則對其任意子族的聯集封閉；∅ 的成員條件用來處理空子族。本稿沒有另證或使用這個一般命題，τ₁ 的完整證明仍採鏈引理並單獨處理空族。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 4da430d185bcefe3f83821030d9b54994119c5304ce3b95397b135d2151f8de7
• original source SHA-256: 9fc206f52faa8c93d175434ba7de7802035b74beb7ba12cd2a3c31cc736a538d
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）