# 從原覆蓋索引選取子覆蓋

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

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

derivation-mko-open-cover-and-subcover-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

核對 K={a,b} 的指定開覆蓋與子覆蓋索引。

只核這個覆蓋，不以單一成功推出一般緊緻性。





## 已知條件與符號


- sets
- topology
- definition_here


- G1 — X={a,b,c}，tau=全部 X 的子集；K={a,b}。
- G2 — 有序族 U_1={a}、U_2={b}、U_3={a,b}、U_4={c}。原始選取索引 (3,3) 正規化為 {3}。


- K — 覆蓋目標
- U_i — 原覆蓋成員
- I — 正規化索引集





## 規則與來源


- mko_definition · cited — 完整核每個成員為開集、目標包含與選取索引。某一供給覆蓋有有限子覆蓋只證該覆蓋，不證空間緊緻。 · mko-open-cover-and-subcover
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。
- definition_here · prerequisite — 開覆蓋各成員開且聯集包含目標；子覆蓋取自原索引子集且仍覆蓋同一目標。





## 逐步主鏈

S01 · implies操作前

\tau=\mathcal P(X)

操作後

\tau=\{\varnothing,\{a\},\{b\},\{c\},\{a,b\},\{a,c\},\{b,c\},X\}

條件：無

規則：topology · 依賴：G1

葉節點依據：topology

列出全部八個子集。任意聯與有限交仍為 X 子集，因此確為拓撲。



S02 · implies操作前

i\in\{1,2,3,4\}

操作後

U_i\in\tau

條件：無

規則：sets · 依賴：G1, G2, S01

葉節點依據：sets

逐個成員都在八項開集清單，含不與 K 相交的 U_4 也合法。



S03 · implies操作前

\bigcup_{i=1}^4 U_i

操作後

\{a\}\cup\{b\}\cup\{a,b\}\cup\{c\}=X

條件：無

規則：sets · 依賴：G2

葉節點依據：sets

按原有序族取聯，覆蓋了 X 因而也覆蓋 K。



S04 · implies操作前

(3,3)

操作後

I=\{3\}\subseteq\{1,2,3,4\}

條件：無

規則：sets · 依賴：G2

葉節點依據：sets

去除重複索引不會改變選取集合的聯。



S05 · equivalent操作前

\bigcup_{i\in I}U_i

操作後

U_3=\{a,b\}=K

條件：無

規則：sets · 依賴：G1, G2, S04

葉節點依據：sets

原族中的第三個集合單獨已覆蓋目標。



S06 · definition操作前

I=\{3\},\quad K\subseteq\bigcup_{i\in I}U_i

操作後

(U_i)_{i\in I}\text{ is a finite open subcover}

條件：無

規則：definition_here · 依賴：S02, S04, S05

葉節點依據：definition_here

開性由原成員繼承，且一個索引是有限集合。



S07 · implies操作前

J=\{1\}

操作後

\bigcup_{i\in J}U_i=\{a\}\not\supseteq K

條件：無

規則：sets · 依賴：G1, G2

葉節點依據：sets

以漏掉 b 的選取作負向核對；原覆蓋合法不代表任意子族仍覆蓋。



S08 · implies操作前

\exists I\text{ finite for this supplied cover}

操作後

\text{this supplied cover has a finite subcover}

條件：無

規則：sets · 依賴：S06

葉節點依據：sets

結論只保留已核的覆蓋；每個開覆蓋的全稱命題是另一責任。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S06 — 沒有把存在一個成功選取反轉成對所有覆蓋的證明。
- S07 · premise_audit · G1, G2 — 失敗原因是缺 b，不是 U_1 不開。
- S06 · premise_audit · S02, S04, S05 — 需要開性、來源索引與覆蓋三件事，先前步驟各自提供。
- S05 · inverse_equivalence · G1, G2, S04 — 將正規化後索引回讀原族而不是直接憑目標造一個集合。
- S04 · premise_audit · G2 — 索引 3 存在於原族；沒有加入新集合。
- S03 · premise_audit · G2 — 覆蓋目標只需 K 包含於聯集，不需恰等。
- S02 · premise_audit · G1, G2, S01 — 開覆蓋不要求每個成員包含於 K，也不要求每個都必要。
- S01 · premise_audit · G1 — 不是把供給的四個覆蓋成員當完整拓撲。





## 錯誤控制與反例

索引溯源每次選取都由原有序族讀回成員。

量詞不升格一次子覆蓋成功與每個開覆蓋均成功分開。


- 選 {a,b,c} 也算原覆蓋的子覆蓋。 → reject — X 雖然開但不在原族中，子覆蓋不能新增成員。
- {1} 覆蓋 K。 → reject — 聯集漏掉 b。
- 這一次成功已證所有空間緊緻。 → reject — 只核一個供給覆蓋，沒有全稱量詞。





## 結論與限制

{3} 是合法有限子覆蓋索引，而 {1} 不是。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 5da7ac00e9a6cf40783fb48632b4b9388c717c3012a47aff481fcdd179f5f222
- original source SHA-256: 5da7ac00e9a6cf40783fb48632b4b9388c717c3012a47aff481fcdd179f5f222
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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