# 子集合

A⊆B 表示 A 的每個元素也都是 B 的元素。

mko-subset · definition · v0.10.0



## 數學敘述

給定同一論域中的集合 A、B，A⊆B 當且僅當對每個對象 x，若 x∈A，則 x∈B。





## 代表公式（精確 TeX）

A\subseteq B





## 成立條件


- A 與 B 是同一 ambient type 或同一明示論域中的集合。





## 符號作用域


- A — 候選子集合
- B — 候選母集合
- ⊆ — 非嚴格子集合關係





## 直觀、定義與常見誤解

要證明 A⊆B，必須從任意 x∈A 出發，說明同一個 x 也屬於 B；只列出一個共同元素並不充分。

A⊆B 允許 A=B，所以它是非嚴格包含。若要表達 A 是 B 的嚴格子集合，還必須排除 A=B。

x∈A 與 A⊆B 的型別角色不同：前者比較元素與集合，後者比較兩個集合。在 Lean 的 Set α 中，兩個集合也必須共享元素型別 α。

常見誤解是把 x∈A 與 {x}⊆A 混為同一語句、認為 A⊆B 必須 A≠B，或只檢查部分元素便斷言包含。





## 已採用的推導導讀

[子集合：以任意元素證明包含，並以反例否定包含](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-subset-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [集合隸屬](https://ocme.evemisslab.com/zh-Hant/mko/mko-set-membership/) — 子集合以每個元素的隸屬蘊含關係定義。





## 驗證界線

本條目是子集合定義的 AI 候選；有限列舉可重算具體包含關係，但不能證成任意集合上的普遍性質。

not_formalized

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





## 下一個義務

綁定 Set.Subset 的精確定義展開、Mathlib 版本與 axiom receipt，並保持非嚴格包含、嚴格包含及集合相等三者分離。





## 同源結構化資料

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

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/subset.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-subset/index.md)