集合運算

數學敘述

對同一論域中的集合 A、B，聯集收納至少屬於其中一集的元素，交集收納同時屬於兩集的元素，差集 A\B 收納屬於 A 但不屬於 B 的元素；補集必須相對明示全集 U，以 U\A 表示。

代表公式（精確 TeX）

A\cup B

成立條件

• A 與 B 是同一 ambient type 或同一明示論域 U 中的集合。
• 使用補集時，全集 U 或 ambient type 已被明確指定。

符號作用域

• A — 左集合
• B — 右集合
• ∪ — 聯集運算

直觀、定義與常見誤解

A∪B 包含 A 或 B 中出現的所有元素，重複出現仍只算一個集合元素；A∩B 只保留兩集共有的元素。

A\B 具有方向性，只保留屬於 A 且不屬於 B 的元素，因此通常不同於 B\A。

補集不是脫離論域的絕對操作。在有限題目中必須先列出全集 U，A 的相對補集才是 U\A；在 Lean 的 Set α 中，補集相對 ambient type α 的 univ 解讀。

常見誤解是把聯集和交集互換、認為 A\B 與 B\A 相同，或在沒有指定全集時直接列出補集。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 集合隸屬 — 四種集合運算都以元素是否隸屬輸入集合來定義輸出集合。

驗證界線

本條目是集合運算的 AI 候選；有限集合列舉只能檢查具體例子，不構成四種運算普遍性質的證明。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。

下一個義務

分別綁定 Set.mem_union、intersection membership、Set.mem_sdiff 與 Set.mem_compl_iff 的精確聲明、來源、版本與 axiom receipt。

同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。