# 拓撲空間：完整驗證三點集合上的一個鏈狀開集族，並辨認非拓撲 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-topological-space/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-topological-space-01 · production-20261019-adopted-96 ## 目標與範圍 設 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 — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - 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 的子集）。 ## 逐步主鏈 S01 · definition操作前 \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 條件：無 規則：mko_topology_def · 依賴：G1, G2, mko_topology_def 葉節點依據：mko_topology_def + def_unfold 依 MKO 的定義寫出要驗證的條件：每個成員是 X 的子集合；∅ 與 X 在 τ 中；每個子族（包括空族與無窮子族）的聯集在 τ 中；每個有限子族（包括空族）的交集在 τ 中，空族交集按 X 解讀（G2）。 S02 · implies操作前 \tau_1=\{\varnothing,\{a\},\{a,b\},X\} 操作後 \tau_1\subseteq\mathcal{P}(X) 條件：無 規則：subset_def · 依賴：G1, subset_def 葉節點依據：subset_def 四個成員的元素都在 a、b、c 之中，所以每個成員都是 X 的子集合（MKO 假設 a1）。 S03 · implies操作前 \mathcal{S}=\varnothing\subseteq\tau_1 操作後 \bigcup\varnothing=\varnothing\in\tau_1,\quad \bigcap\varnothing=X\in\tau_1 條件：無 規則：family_ops · 依賴：G2, family_ops, S02 葉節點依據：family_ops + set_extensionality 空族沒有成員，沒有任何 x 屬於某個成員，所以 ⋃∅=∅；而「對每個 A∈∅ 都有 x∈A」對每個 x∈X 空真成立，所以 ⋂∅=X。∅ 與 X 都列在 τ₁ 中。可見公理「∅∈τ、X∈τ」正是聯集條件與交集條件的空族情形。 S04 · implies操作前 \varnothing,\ \{a\},\ \{a,b\},\ X 操作後 \varnothing\subseteq\{a\}\subseteq\{a,b\}\subseteq X 條件：無 規則：subset_def · 依賴：G1, subset_def 葉節點依據：subset_def + logic_chain 逐一檢查包含：∅ 沒有元素；a∈{a,b}；a、b∈X。由 ⊆ 的遞移性，τ₁ 中任兩成員都可比較：τ₁ 是一條鏈。 S05 · implies操作前 \varnothing\neq\mathcal{S}\subseteq\tau_1 操作後 \mathcal{S}\ \text{has a largest member}\ M\ \text{and a smallest member}\ m 條件：\mathcal{S}\neq\varnothing 規則：L_chain_extremes · 依賴：S04, L_chain_extremes 葉節點依據：nat_induction + subset_def + case_analysis τ₁ 只有 4 個成員，所以每個子族都有限；子族的成員仍兩兩可比較（S04）。依引理 L_chain_extremes（S05.1 到 S05.3 證明），每個非空子族都有最大與最小成員。 S06 · implies操作前 M,\ m\ \text{largest and smallest in}\ \mathcal{S} 操作後 \bigcup\mathcal{S}=M,\quad \bigcap\mathcal{S}=m 條件：\mathcal{S}\neq\varnothing 規則：L_chain_union · 依賴：S05, L_chain_union 葉節點依據：set_extensionality + family_ops + subset_def 依引理 L_chain_union（S06.1、S06.2 證明），非空子族的聯集是它的最大成員，交集是它的最小成員。 S07 · case_split操作前 \mathcal{S}\subseteq\tau_1\ \text{arbitrary} 操作後 \bigcup\mathcal{S}\in\tau_1 條件：無 規則：case_analysis · 依賴：S03, S05, S06 葉節點依據：case_analysis + family_ops 分兩種情況：𝒮 為空時 ⋃𝒮=∅∈τ₁（S03）；𝒮 非空時 ⋃𝒮=M（S06），而 M∈𝒮⊆τ₁。兩種情況涵蓋 τ₁ 的每個子族，所以 τ₁ 對任意聯集封閉。 S08 · case_split操作前 \mathcal{S}\subseteq\tau_1\ \text{finite} 操作後 \bigcap\mathcal{S}\in\tau_1 條件：無 規則：case_analysis · 依賴：S03, S05, S06 葉節點依據：case_analysis + family_ops 𝒮 為空時 ⋂𝒮=X∈τ₁（S03）；𝒮 非空時 ⋂𝒮=m（S06），而 m∈τ₁。所以 τ₁ 對有限交集封閉。 S09 · implies操作前 \tau_1\subseteq\mathcal{P}(X),\ \text{unions and finite intersections closed} 操作後 (X,\tau_1)\ \text{is a topological space} 條件：無 規則：mko_topology_def · 依賴：S02, S03, S07, S08, mko_topology_def 葉節點依據：mko_topology_def + and_intro_elim S02、S03、S07、S08 給出定義的全部條件。計數核對：τ₁ 有 4 個成員，共 2⁴=16 個子族；S03 處理空族 1 個，S07、S08 透過 S05、S06 處理其餘 15 個非空子族。這是完整枚舉語義下的證明，不是抽查。 S10 · implies操作前 \{a\},\ \{b\}\in\tau_2 操作後 \{a\}\cup\{b\}=\{a,b\}\notin\tau_2 條件：無 規則：set_operations_def · 依賴：G1, set_operations_def 葉節點依據：set_operations_def + set_extensionality + contradiction {a}∪{b}={a,b}。逐一比較 τ₂ 的四個成員：{a,b}≠∅（含 a）；≠{a}（含 b 且 b≠a）；≠{b}（含 a 且 a≠b）；≠X（c∉{a,b}，因 c≠a、c≠b）。所以子族 {{a},{b}} 的聯集不在 τ₂ 中，τ₂ 不是拓撲。 S11 · implies操作前 \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 條件：無 規則：set_operations_def · 依賴：G1, set_operations_def 葉節點依據：set_operations_def + numeric_evaluation τ₂ 含 ∅ 與 X；兩兩交集：{a}∩{b}=∅，任何 A∩X=A，A∩∅=∅，A∩A=A，都在 τ₂ 中（不同成員共 C(4,2)=6 對）。所以只檢查交集或只檢查 ∅、X 會誤判 τ₂ 為拓撲；每一類條件都要檢查。 S12 · implies操作前 \{\varnothing,X\},\ \tau_1,\ \mathcal{P}(X) 操作後 \{\varnothing,X\}\subsetneq\tau_1\subsetneq\mathcal{P}(X) 條件：無 規則：subset_def · 依賴：S09, subset_def 葉節點依據：subset_def + set_operations_def + family_ops 不可分拓撲 {∅,X} 的兩個成員都在 τ₁ 中，而 {a}∈τ₁ 不在其中；τ₁ 的成員都是 X 的子集合，而 {b}∈P(X) 不在 τ₁ 中。P(X) 有 2³=8 個成員，是拓撲：X 的子集合的聯集與交集仍是 X 的子集合。{∅,X} 也是拓撲：其子族的聯集只能是 ∅ 或 X，交集也是。所以同一個 X 上至少有三個不同的拓撲，τ₁ 比不可分拓撲細、比離散拓撲粗。 S13 · implies操作前 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}} 條件：無 規則：finite_sets · 依賴：G3, finite_sets 葉節點依據：finite_sets + case_analysis + set_operations_def ∅ 有限，ℕ 直接列入，所以兩者都在 τ_fin。兩兩聯集：A、B 都有限時 A∪B 有限；其一為 ℕ 時聯集為 ℕ。兩兩交集：其一有限時交集是有限集合的子集合，仍有限；兩者都是 ℕ 時交集為 ℕ。所以 τ_fin 對兩兩聯集與兩兩交集封閉。 S14 · implies操作前 \mathcal{S}=\{\{2k\}:k\in\mathbb{N}\}\subseteq\tau_{\mathrm{fin}} 操作後 \bigcup\mathcal{S}=E\notin\tau_{\mathrm{fin}} 條件：無 規則：family_ops · 依賴：G3, family_ops 葉節點依據：family_ops + contradiction 每個單點集 {2k} 有限，屬於 τ_fin。依聯集定義，⋃𝒮=E 是全部偶數。E 不在 τ_fin 中：S14.1 證 E≠ℕ，S14.2 證 E 不是有限集合。所以 τ_fin 對這個無窮子族的聯集不封閉，不是拓撲，雖然 S13 的兩兩檢查都通過。 S15 · implies操作前 \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) 條件：無 規則：and_intro_elim · 依賴：S09, S10, S12, S14 葉節點依據：and_intro_elim 合併：S09 給 (1)；S10 給 (2)（S11 說明它通過的檢查）；S12 給 (3)；S13、S14 給 (4)。 ## 局部子步與引理 S05.1 · induction_base操作前 |\mathcal{S}|=1,\ \mathcal{S}=\{A\} 操作後 M=m=A 條件：無 規則：subset_def · 依賴：subset_def 葉節點依據：subset_def 只有一個成員 A 時，A⊆A，所以 A 同時是最大與最小成員。 S05.2 · induction_step操作前 |\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} 條件：n\ge 1 規則：case_analysis · 依賴：subset_def, case_analysis 葉節點依據：case_analysis + subset_def + logic_chain 取 A∈𝒮，𝒮′=𝒮∖{A} 有 n 個成員且仍成鏈，依歸納假設有最大 M′ 與最小 m′。A 與 M′ 可比較：若 A⊆M′，M′ 是 𝒮 的最大成員；若 M′⊆A，則對 B∈𝒮′ 有 B⊆M′⊆A，A 是最大成員。最小成員同理比較 A 與 m′。 S05.3 · implies操作前 P(1)\ \land\ \forall n\ge 1\,(P(n)\Rightarrow P(n+1)) 操作後 \forall n\ge 1:\ P(n) 條件：無 規則：nat_induction · 依賴：S05.1, S05.2, nat_induction 葉節點依據：nat_induction 令 P(n) 為「每個 n 個成員的鏈都有最大與最小成員」。由 S05.1、S05.2 與數學歸納原理，P(n) 對每個 n≥1 成立。S05.1 到 S05.3 證得引理 L_chain_extremes。 S06.1 · implies操作前 M\in\mathcal{S},\ \forall A\in\mathcal{S}:\ A\subseteq M 操作後 \bigcup\mathcal{S}=M 條件：無 規則：set_extensionality · 依賴：family_ops, set_extensionality 葉節點依據：set_extensionality + family_ops M∈𝒮，所以 M⊆⋃𝒮；若 x∈⋃𝒮，則 x∈A 對某個 A∈𝒮，而 A⊆M，故 x∈M，即 ⋃𝒮⊆M。兩向包含得相等。 S06.2 · implies操作前 m\in\mathcal{S},\ \forall A\in\mathcal{S}:\ m\subseteq A,\ m\subseteq X 操作後 \bigcap\mathcal{S}=m 條件：無 規則：set_extensionality · 依賴：family_ops, set_extensionality 葉節點依據：set_extensionality + family_ops m∈𝒮，所以 ⋂𝒮⊆m；若 x∈m，則 x∈X 且 x 屬於每個 A∈𝒮（因 m⊆A），故 x∈⋂𝒮。兩向包含得相等。S06.1、S06.2 證得引理 L_chain_union。 S14.1 · implies操作前 1\in E\ ? 操作後 1\notin E,\ \text{so}\ E\neq\mathbb{N} 條件：無 規則：set_extensionality · 依賴：G3 葉節點依據：set_extensionality + order_basics + case_analysis 若 1=2k，k=0 給 0，k≥1 給至少 2，都不是 1；所以 1∉E，而 1∈ℕ，故 E≠ℕ。 S14.2 · implies操作前 E\ \text{finite}\ ? 操作後 E\ \text{is infinite} 條件：無 規則：contradiction · 依賴：G3, finite_sets 葉節點依據：contradiction + finite_sets + distributive 假設 E 有限。0∈E，所以 E 非空，依 finite_sets 有最大元素 m=2j。但 m+2=2(j+1)∈E 且 m+2>m，與 m 最大矛盾。所以 E 是無窮集合。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-topological-space-01.json)