# 三集合全部七個交集項 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-inclusion-exclusion-principle/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-inclusion-exclusion-principle-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 完整核交替和與每元素的重數。 indexed有限家族，重複sets仍按indices處理。 ## 已知條件與符號 - work - G1 — A={1,2,3}，B={2,3,4}，C={3,4,5}。 - r — 元素所屬indexed sets數 ## 規則與來源 本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。 - mko_definition · cited — 對每個非空 I⊆[n] 使用 (-1)^(|I|+1)|intersection_i in I A_i|；odd-order 正、even-order 負。重複 sets 仍按 indices 處理，空交集對計數和貢獻 0。空家族的聯集為空集，其基數與容斥和皆為 0。只用 singles/pairs 對 n≥3 不是一般的 exact inclusion-exclusion，截斷只能另稱 Bonferroni bound。 · mko-inclusion-exclusion-principle - work · prerequisite — 集合union與intersection、有限和按元素計重；二項式identity(1-1)^r=sum_j(-1)^j comb(r,j)為明示前提。 ## 逐步主鏈 S01 · implies操作前 A\cup B\cup C 操作後 \{1,2,3,4,5\},\quad|A\cup B\cup C|=5 條件：無 規則：work · 依賴：G1, work 葉節點依據：work 先由完整元素清單直接算union作獨立核對。 S02 · implies操作前 |A|,|B|,|C| 操作後 3,3,3 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work 三個一階項為正，總和9。 S03 · implies操作前 A\cap B,A\cap C,B\cap C 操作後 \{2,3\},\{3\},\{3,4\} 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work 完整列三個二階交集，大小2、1、2。 S04 · implies操作前 A\cap B\cap C 操作後 \{3\},\quad|A\cap B\cap C|=1 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work 唯一三階交集必須加回。 S05 · implies操作前 3+3+3-2-1-2+1 操作後 5=|A\cup B\cup C| 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work 七個nonempty index subsets全部使用。 S06 · implies操作前 x\text{ belongs to }r\ge1\text{ indexed sets} 操作後 \sum_{j=1}^{r}(-1)^{j+1}\binom rj=1-(1-1)^r=1 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 每個在union的元素於交替和中淨算一次，給有限公式的逐元素證明。 S07 · implies操作前 \text{singles minus pairs only} 操作後 9-5=4\ne5 條件：無 規則：work · 依賴：G1, S06, work 葉節點依據：work 此例明確顯示三階不能省，pairwise truncation不是exact式。 S08 · implies操作前 (A,A)\text{ indexed twice};\quad n=0 操作後 |A|+|A|-|A|=|A|;\quad|\bigcup\varnothing|=0 條件：無 規則：work · 依賴：G1, S07, work 葉節點依據：work 重複家族仍按indices正確消重；空家族sum與union大小皆零。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S07, work — 相同set不等於省略一個index責任。 - S07 · premise_audit · G1, S06, work — 若稱Bonferroni bound須另標示，而非等號。 - S06 · premise_audit · G1, S05, work — 不在union的r=0元素貢獻零另處理。 - S05 · premise_audit · G1, S04, work — 3+3+1=7與2³-1一致。 - S04 · premise_audit · G1, S03, work — 不是因pairwise intersections已列就省triple。 - S03 · premise_audit · G1, S02, work — 二階項的符號為負。 - S02 · premise_audit · G1, S01, work — indexed entries各算一次。 - S01 · premise_audit · G1, work — 沒有只靠公式預寫預期結果。 ## 錯誤控制與反例 七項按index subsets而非不同集合值枚舉。 逐元素r≥1用1-(1-1)^r，r=0另給零。 - 三集合只要singles減pairs就exact。 → reject — 本例4不等union size5。 - triple交集應減。 → reject — 三階為奇數，符號正。 - 重複兩set就直接把union計兩倍。 → reject — 二階交集恰扣回一份。 ## 結論與限制 全部七項給union size5；每元素淨重數證一般有限家族公式。 ## 驗證及來源綁定 3 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: ea75129552baa4d33afae410265a8e2ec2eda5b1a8669c83da8afed4efc43c95 - original source SHA-256: d12d13f29453c49f15f41deea45201369e57e7476d15786a97750ca414dc608a - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-inclusion-exclusion-principle-01.json)