# 邊界與補集的精確對照 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-topological-boundary/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-topological-boundary-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 計算鏈狀拓撲中 A={b} 與其補集的邊界。 完整有限開閉集計算，未使用度量或圖形。 ## 已知條件與符號 - sets - topology - definition_here - G1 — X={a,b,c}，tau={空集,{a},{a,b},X}，A={b}，D=X\A={a,c}。 - \partial A — 拓撲邊界 - D — 相對 X 的補集 ## 規則與來源 - mko_definition · cited — 完整驗有限拓撲後精確計算closure與interior。保留boundary(A)=boundary(complement A)、空集與全空間邊界，以及拓撲相對性。neighborhood contact若使用必須枚舉全部open neighborhoods。 · mko-topological-boundary - 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 · 依賴：G1, S01 葉節點依據：definition_here 相對 X 逐項補集得到全部閉集。 S03 · definition操作前 F\supseteq A,\quad F\in\mathcal F 操作後 \overline A=X\cap\{b,c\}=\{b,c\} 條件：無 規則：definition_here · 依賴：G1, S02 葉節點依據：definition_here 含 b 的閉集恰為 X 與 {b,c}。 S04 · definition操作前 U\subseteq A,\quad U\in\tau 操作後 A^\circ=\bigcup\{\varnothing\}=\varnothing 條件：無 規則：definition_here · 依賴：G1, S01 葉節點依據：definition_here 所有非空開集含 a，故沒有非空開子集落在 A 中。 S05 · definition操作前 \partial A=\overline A\setminus A^\circ 操作後 \partial A=\{b,c\} 條件：無 規則：definition_here · 依賴：S03, S04 葉節點依據：definition_here 直接按邊界定義作差集。 S06 · definition操作前 D=\{a,c\} 操作後 \overline D=X,\quad D^\circ=\{a\} 條件：無 規則：definition_here · 依賴：G1, S01, S02 葉節點依據：definition_here 含 a,c 的唯一閉集為 X；包含於 D 的開集是空集與 {a}。 S07 · implies操作前 \partial D=\overline D\setminus D^\circ 操作後 \partial D=\{b,c\}=\partial A=\overline A\cap\overline D 條件：無 規則：sets · 依賴：S05, S06 葉節點依據：sets 補集邊界及雙閉包交集都給同一結果。 S08 · implies操作前 \overline\varnothing=\varnothing,\ \varnothing^\circ=\varnothing,\ \overline X=X=X^\circ 操作後 \partial\varnothing=\partial X=\varnothing 條件：無 規則：sets · 依賴：S01, S02 葉節點依據：sets 空集與全集的邊界都空，避免把全空間外緣當未定義的幾何概念。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · S01, S02 — 每個閉包與內部均可由已列族直接核對。 - S07 · premise_audit · S05, S06 — 三個集合等式逐元素核對，只聲稱此明示例子。 - S06 · premise_audit · G1, S01, S02 — 對 D 重新完整列舉，不由圖形猜對稱。 - S05 · premise_audit · S03, S04 — 結果不必是 A 的子集；c 在邊界但不在 A。 - S04 · premise_audit · G1, S01 — 並未把集合自身誤當成開集。 - S03 · premise_audit · G1, S02 — {c} 與空集不含 b，故閉超集枚舉完整。 - S02 · premise_audit · G1, S01 — 每個補集再補一次恰好回原開集。 - S01 · premise_audit · G1 — 此族完整列出四項，鏈性足以核全部公理。 ## 錯誤控制與反例 兩側獨立計算對 A 及補集分別列完整開子集與閉超集。 不換全集差集和補集固定相對 X。 - 邊界必包含於 A。 → reject — c 屬邊界卻不屬 A。 - X 的邊界是 X。 → reject — X 的閉包及內部均 X，作差後為空。 - 此結果由三點之間的距離決定。 → reject — 未指定度量，答案來自所列拓撲。 ## 結論與限制 兩個互補集合的邊界皆 {b,c}；空集及 X 邊界皆空。 ## 驗證及來源綁定 0 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 21eba37c5fc910925cb200b0b393070d907805f2655a1be31714240ec9c5add6 - original source SHA-256: 21eba37c5fc910925cb200b0b393070d907805f2655a1be31714240ec9c5add6 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-topological-boundary-01.json)