集合運算：在明示全集中計算聯集、交集、差集與補集

目標與範圍

全集 U={1,2,3,4,5,6,7,8}，A={2,4,6,8}，B={3,4,5,6}。逐元素算出 A∪B、A∩B、A∖B、B∖A、U∖A、U∖B；說明 A∖B≠B∖A；說明全集換成 U′={1,2,3,4,5,6,7,8,9,10} 時 A 的補集改變；對任意集合證明 U∖(A∪B)=(U∖A)∩(U∖B) 並以本例核對；再以 A∪B=A∪(B∖A) 說明聯集為何有 6 個元素而不是 8 個。

只處理一個明示全集中的有限集合（MKO 假設 a1、a2）。運算由成員條件定義並逐元素計算；德摩根律以一般論證證明，具體例子只作核對。不綁定 Lean 的 Set.mem_union 等聲明；不改動 canonical MKO 或英文 edition。

已知條件與符號

• set_operations_def
• set_extensionality
• subset_def
• finite_set_listing
• finite_counting_basics
• de_morgan_logic

• G1 — 全集 U={1,2,3,4,5,6,7,8}（MKO 假設 a2：使用補集前已明示全集）。
• G2 — A={2,4,6,8}，B={3,4,5,6}。
• G3 — 比較用的另一個全集 U′={1,2,3,4,5,6,7,8,9,10}。

• U,\ U' — 兩個明示全集
• A\cup B — 聯集：至少屬於其中一集
• A\cap B — 交集：同時屬於兩集
• A\setminus B — 差集：屬於 A 但不屬於 B
• U\setminus A — A 相對於全集 U 的補集
• |X| — 有限集合 X 的元素個數
• (T,F) — 成員表的一列：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，即兩者有相同元素。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• mko_set_ops · cited — 對同一論域中的集合 A、B，聯集收納至少屬於其中一集的元素，交集收納同時屬於兩集的元素，差集 A∖B 收納屬於 A 但不屬於 B 的元素；補集必須相對明示全集 U，以 U∖A 表示。 · mko-set-operations
• finite_set_listing · prerequisite — 列舉集合：x 屬於以列舉方式給出的有限集合，當且僅當 x 等於所列對象之一；列舉的次序與重複不改變集合，例如 {4,4,6}={4,6}。
• L_ops_in_U · lemma — 若 A⊆U 且 B⊆U，則 A∪B、A∩B、A∖B、B∖A 都是 U 的子集合。
• L_de_morgan_set · lemma — 對任意集合 U、A、B：U∖(A∪B)=(U∖A)∩(U∖B)。
• L_union_split · lemma — 對任意集合 A、B：A∪B=A∪(B∖A)，且 A∩(B∖A)=∅。

逐步主鏈

\text{a universe and two sets}

U=\{1,2,3,4,5,6,7,8\},\ A=\{2,4,6,8\},\ B=\{3,4,5,6\}

A=\{2,4,6,8\},\ B=\{3,4,5,6\},\ U=\{1,2,3,4,5,6,7,8\}

A\subseteq U,\ B\subseteq U

A\subseteq U,\ B\subseteq U

A\cup B,\ A\cap B,\ A\setminus B,\ B\setminus A\subseteq U

x\in U

1{:}(F,F),\ 2{:}(T,F),\ 3{:}(F,T),\ 4{:}(T,T),\ 5{:}(F,T),\ 6{:}(T,T),\ 7{:}(F,F),\ 8{:}(T,F)

A\cup B

\{2,3,4,5,6,8\}

A\cap B

\{4,6\}

A\setminus B

\{2,8\}

B\setminus A

\{3,5\}

A\setminus B=\{2,8\},\ B\setminus A=\{3,5\}

A\setminus B\neq B\setminus A

U\setminus A,\ U\setminus B

U\setminus A=\{1,3,5,7\},\ U\setminus B=\{1,2,7,8\}

U'\setminus A

U'\setminus A=\{1,3,5,7,9,10\}\neq U\setminus A

U\setminus(A\cup B)

(U\setminus A)\cap(U\setminus B)

U\setminus\{2,3,4,5,6,8\},\quad \{1,3,5,7\}\cap\{1,2,7,8\}

\{1,7\}=\{1,7\}

A\cup B

A\cup(B\setminus A)\ \text{with}\ A\cap(B\setminus A)=\varnothing

|A\cup B|=|A\cup(B\setminus A)|

|A\cup B|=|A|+|B\setminus A|=4+2=6

\text{membership table of }U

A\cup B=\{2,3,4,5,6,8\},\ A\cap B=\{4,6\},\ A\setminus B=\{2,8\},\ B\setminus A=\{3,5\},\ U\setminus A=\{1,3,5,7\},\ U\setminus B=\{1,2,7,8\}

局部子步與引理

x\in A\cup B

x\in U

x\in A\cap B\ \lor\ x\in A\setminus B\ \lor\ x\in B\setminus A

x\in U

x\in U\setminus(A\cup B)

x\in U\land\neg(x\in A\lor x\in B)

x\in U\land\neg(x\in A\lor x\in B)

x\in U\land x\notin A\land x\notin B

x\in U\land x\notin A\land x\notin B

x\in(U\setminus A)\cap(U\setminus B)

x\in A\lor(x\in B\land x\notin A)

x\in A\lor x\in B

x\in A\cap(B\setminus A)

A\cap(B\setminus A)=\varnothing

逐步反向審查

• S16 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S10, S11, S13, S15, and_intro_elim — 目標 G 是題目各項結論的合取；每一項都由所列步驟從已知正向得到，此步只做合取，沒有把 G 當作前提。
• S15 · premise_audit · S14, finite_counting_basics — 加法公式只適用於不相交的集合，所以必須先有 S14.2 的 A∩(B∖A)=∅；直接把 A、B 的大小相加不合法，因為 A∩B≠∅。
• S14.2 · premise_audit · set_operations_def, contradiction — 只需兩個定義展開與矛盾；不宣稱 A∩B=∅（本例 A∩B={4,6}）。
• S14.1 · inverse_equivalence · case_analysis, set_operations_def — 每種情況下兩邊都等價，且兩種情況窮盡，所以整體等價雙向成立。
• S14 · inverse_equivalence · L_union_split — 引理給出集合相等，雙向成立；不相交另由 S14.2 給出。
• S13 · premise_audit · S05, S10, S12, set_operations_def — 這是一個例子的核對，可以獨立重算；它不取代 S12 的一般證明，一個例子也不能證明德摩根律。
• S12.3 · inverse_equivalence · and_intro_elim, set_operations_def, set_extensionality — 合取的重組與重複都是雙向的；每個 x 兩邊同真同假，所以兩集合相等。
• S12.2 · inverse_equivalence · de_morgan_logic — 德摩根律本身是等價，雙向成立。
• S12.1 · inverse_equivalence · set_operations_def — 兩個定義展開都是雙向的。
• S12 · inverse_equivalence · L_de_morgan_set — 引理證明的是集合相等，由逐元素的雙向等價得到。
• S11 · premise_audit · G3, set_operations_def, set_extensionality — 需要 U′ 明示；單一見證 9 足以否定兩個補集相等。
• S10 · inverse_equivalence · mko_set_ops, set_operations_def, set_extensionality — U∖A 由成員條件逐元素決定，雙向對照；U 以外的對象不屬於 U∖A。
• S09 · premise_audit · S07, S08, set_extensionality — 一個只屬於其中一邊的元素就足以否定相等。不宣稱對所有集合 A∖B 與 B∖A 都不等：A=B 時兩者都是 ∅。
• S08 · inverse_equivalence · set_operations_def, set_extensionality, S03 — 同 S05，逐元素雙向對照。
• S07 · inverse_equivalence · set_operations_def, set_extensionality, S03 — 同 S05，逐元素雙向對照。
• S06 · inverse_equivalence · set_operations_def, set_extensionality, S03 — 同 S05，逐元素雙向對照。
• S05 · inverse_equivalence · set_operations_def, set_extensionality, S03 — 兩邊對每個對象的成員判定相同：在 U 中逐列對照，在 U 外兩邊都不含它（S03）；依集合相等判準，雙向成立。
• S04 · premise_audit · finite_set_listing, S03 — 每一列都可以對照列舉重查；表格完整涵蓋 U，所以沒有遺漏的元素。
• S03.2 · premise_audit · set_operations_def, and_intro_elim, subset_def — 只用到從合取中取出一項；不宣稱反向（U 的元素不必在這些集合中）。
• S03.1 · premise_audit · set_operations_def, subset_def, case_analysis — 兩種情況涵蓋「或」的全部可能；每種情況各用一個包含假設。
• S03 · premise_audit · S02, L_ops_in_U — 需要 A⊆U 與 B⊆U（S02）；若 A 有 U 以外的元素，只檢查 U 會漏掉聯集的元素。
• S02 · premise_audit · subset_def, finite_set_listing — 這是完整窮舉，不是抽樣：A、B 的每個元素都被檢查。反向 U⊆A 不宣稱（1∈U 但 1∉A）。
• S01 · premise_audit · G1, G2, def_intro, finite_set_listing — 此步只寫出資料，不推出新事實；全集已明示，符合假設 a2。

錯誤控制與反例

聯集與交集互換

MKO 指出常見誤解是把聯集和交集互換。聯集對應「或」（至少屬於其一），交集對應「且」（同時屬於兩者）。本例 2∈A∪B 但 2∉A∩B，聯集有 6 個元素、交集只有 2 個；算錯時，可回到成員表檢查讀的是「至少一個 T」還是「兩個都是 T」。

差集有方向

MKO 提醒 A∖B 與 B∖A 通常不同。本例 A∖B={2,8} 而 B∖A={3,5}（S07 到 S09），兩者甚至不相交。只有在特殊情況（例如 A=B，兩者都是 ∅）才相等。

補集要先指定全集

MKO 提醒不要在未指定全集時直接列出補集。同一個 A={2,4,6,8}，在 U 中的補集是 {1,3,5,7}，在 U′ 中是 {1,3,5,7,9,10}（S10、S11）。所以必須寫成 U∖A 並先列出 U。

• A∖B=B∖A → reject — 2∈A∖B 但 2∉B∖A（S09）。
• A∩B={2,3,4,5,6,8} → reject — 那是聯集；2∉B，所以 2∉A∩B，正確答案是 {4,6}。
• A∪B 有 |A|+|B|=8 個元素 → reject — 4 與 6 屬於兩集但只算一次；|A∪B|=6（S15）。
• 不必說明全集，A={2,4,6,8} 的補集就是 {1,3,5,7} → reject — 在 U′ 中補集是 {1,3,5,7,9,10}（S11）；補集依賴全集。
• U∖(A∪B)=(U∖A)∪(U∖B) → reject — 右邊是 {1,2,3,5,7,8}，左邊是 {1,7}；正確的德摩根律右邊是交集（S12）。

結論與限制

在全集 U={1,2,3,4,5,6,7,8} 中：A∪B={2,3,4,5,6,8}，A∩B={4,6}，A∖B={2,8}，B∖A={3,5}，U∖A={1,3,5,7}，U∖B={1,2,7,8}。A∖B≠B∖A；全集改為 U′ 時 A 的補集變成 {1,3,5,7,9,10}；U∖(A∪B)=(U∖A)∩(U∖B) 對任意集合成立，本例兩邊都是 {1,7}；|A∪B|=|A|+|B∖A|=6。

• S10、S11 的個數核對用到「A⊆U 時 U 是 A 與 U∖A 的不相交聯集」，這可由 S14 同樣的論證得到，本稿未另立引理。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: c42753a14041612b07055d8ace7c5c9df4c243cd4ab72e79efd18921fc2f0b46
• original source SHA-256: c42753a14041612b07055d8ace7c5c9df4c243cd4ab72e79efd18921fc2f0b46
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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